Revision aa1ca8698adfe929a9eff86ac143eaf90fc3e8ee authored by Jay Bosamiya on 03 June 2019, 21:51:38 UTC, committed by Jay Bosamiya on 03 June 2019, 21:51:38 UTC
1 parent 6055e85
EverCrypt.AEAD.fst.hints
[
"�0�����\f\b9(T�bfS",
[
[
"EverCrypt.AEAD.uu___0",
1,
0,
0,
[
"@query", "equality_tok_EverCrypt.AEAD.Hacl_CHACHA20_POLY1305@tok",
"typing_tok_EverCrypt.AEAD.Hacl_CHACHA20_POLY1305@tok"
],
0,
"e87d11ae4e5a0e70847522e8bec141b3"
],
[
"EverCrypt.AEAD.invariant_s",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"assumption_Spec.AEAD.alg__uu___haseq",
"disc_equation_EverCrypt.AEAD.Hacl_CHACHA20_POLY1305",
"disc_equation_EverCrypt.AEAD.Vale_AES128_GCM",
"disc_equation_EverCrypt.AEAD.Vale_AES256_GCM",
"fuel_guarded_inversion_EverCrypt.AEAD.impl"
],
0,
"c23d72f3c64e8e4c839715c4806f9ff6"
],
[
"EverCrypt.AEAD.invariant",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_EverCrypt.AEAD.state",
"equation_LowStar.Buffer.pointer",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e"
],
0,
"a5909e7cec2414e6bb6cfe5131d1e41c"
],
[
"EverCrypt.AEAD.invariant_loc_in_footprint",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_typing",
"data_elim_EverCrypt.AEAD.Ek", "equation_EverCrypt.AEAD.footprint",
"equation_EverCrypt.AEAD.footprint_s",
"equation_EverCrypt.AEAD.invariant",
"equation_EverCrypt.AEAD.invariant_s",
"equation_EverCrypt.AEAD.state", "equation_EverCrypt.Hash.loc_in",
"equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype",
"equation_Prims.nat",
"fuel_guarded_inversion_EverCrypt.AEAD.state_s",
"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_typing",
"inversion-interp", "kinding_EverCrypt.AEAD.state_s@tok",
"lemma_EverCrypt.AEAD.invert_state_s",
"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",
"typing_EverCrypt.AEAD.footprint_s", "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_not_unused_in"
],
0,
"49b3ded7433cabc75baf05e420cd08de"
],
[
"EverCrypt.AEAD.frame_invariant",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"constructor_distinct_Spec.AEAD.CHACHA20_POLY1305",
"data_elim_EverCrypt.AEAD.Ek", "equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equality_tok_Spec.AEAD.CHACHA20_POLY1305@tok",
"equation_EverCrypt.AEAD.footprint",
"equation_EverCrypt.AEAD.footprint_s",
"equation_EverCrypt.AEAD.invariant",
"equation_EverCrypt.AEAD.invariant_s",
"equation_EverCrypt.AEAD.state", "equation_Lib.IntTypes.byte_t",
"equation_Lib.IntTypes.pub_int_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.AEAD.is_supported_alg",
"fuel_guarded_inversion_EverCrypt.AEAD.state_s",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_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.AEAD.state_s@tok",
"lemma_EverCrypt.AEAD.invert_state_s",
"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_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"typing_EverCrypt.AEAD.footprint_s", "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",
"typing_Spec.AEAD.is_supported_alg"
],
0,
"2a97fed6a899584d2f23d2e6c6cc4853"
],
[
"EverCrypt.AEAD.create_in_st",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_EverCrypt.AEAD.bytes",
"equation_EverCrypt.AEAD.kv_or_dummy", "equation_Spec.AEAD.kv",
"equation_Spec.AEAD.lbytes",
"fuel_guarded_inversion_EverCrypt.AEAD.expanded_key",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
],
0,
"fbffadf6cc26e02b797e3cc634bee39f"
],
[
"EverCrypt.AEAD.create_in_chacha20_poly1305",
1,
0,
0,
[ "@query" ],
0,
"e0ed9d223db5c7be8afdf451d634a090"
],
[
"EverCrypt.AEAD.create_in_chacha20_poly1305",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing",
"constructor_distinct_EverCrypt.AEAD.Hacl_CHACHA20_POLY1305",
"constructor_distinct_EverCrypt.Error.Success",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AEAD.CHACHA20_POLY1305",
"equality_tok_EverCrypt.AEAD.Hacl_CHACHA20_POLY1305@tok",
"equality_tok_EverCrypt.Error.Success@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AEAD.CHACHA20_POLY1305@tok",
"equation_EverCrypt.AEAD.as_kv", "equation_EverCrypt.AEAD.footprint",
"equation_EverCrypt.AEAD.footprint_s",
"equation_EverCrypt.AEAD.freeable",
"equation_EverCrypt.AEAD.freeable_s",
"equation_EverCrypt.AEAD.invariant",
"equation_EverCrypt.AEAD.invariant_s",
"equation_EverCrypt.AEAD.state", "equation_EverCrypt.Hash.fresh_loc",
"equation_EverCrypt.Hash.loc_unused_in",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.live_region",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.pointer_or_null",
"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_Prims.pos",
"equation_Spec.AEAD.expand", "equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.key_length", "equation_Spec.Poly1305.size_key",
"function_token_typing_FStar.Integers.uint_8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"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",
"kinding_EverCrypt.AEAD.state_s@tok",
"lemma_EverCrypt.AEAD.invariant_loc_in_footprint",
"lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_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_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Set.lemma_equal_elim", "lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_addresses_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"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",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_EverCrypt.AEAD.Ek_ek",
"projection_inverse_EverCrypt.AEAD.Ek_impl",
"projection_inverse_EverCrypt.AEAD.Ek_kv",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_601254ebe274211073b2024a11d02039",
"refinement_interpretation_Tm_refine_6959ee19dd537a72ce33d994f7f5e4ee",
"refinement_interpretation_Tm_refine_6f3597d85be0cd881f74d67fa80e3847",
"refinement_interpretation_Tm_refine_916608983647bf7360a3642ca7327620",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_adfe4e4734bd353788723eaa278898e5",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_d185726290ef4a05a84e06a1667d858d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
"typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.live_region",
"typing_FStar.Seq.Base.create", "typing_FStar.Set.singleton",
"typing_LowStar.Buffer.pointer_or_null",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_LowStar.Monotonic.Buffer.loc_unused_in",
"typing_Spec.AEAD.kv", "typing_Spec.Poly1305.size_key",
"typing_tok_EverCrypt.Error.Success@tok",
"typing_tok_Spec.AEAD.CHACHA20_POLY1305@tok"
],
0,
"c70fad6a3377faeac4fda2204ab38220"
],
[
"EverCrypt.AEAD.create_in_chacha20_poly1305",
3,
0,
0,
[ "@query", "projection_inverse_BoxBool_proj_0" ],
0,
"0f996974df14e31bcced9ac7768b2e1d"
],
[
"EverCrypt.AEAD.aes_gcm_alg",
1,
0,
0,
[ "@query", "assumption_Spec.AEAD.alg__uu___haseq" ],
0,
"3968ca7c86d8459a2dc011748c32525c"
],
[
"EverCrypt.AEAD.key_offset",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.AEAD.AES128_GCM",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_GCM",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equation_EverCrypt.AEAD.aes_gcm_alg",
"refinement_interpretation_Tm_refine_703f66a7c02f9a98bc52781f977506bd"
],
0,
"ac0762d30d9b417a4e32a88fef3e3800"
],
[
"EverCrypt.AEAD.ekv_len",
1,
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.Unsigned",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AEAD.AES128_GCM",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_GCM",
"disc_equation_Spec.AEAD.CHACHA20_POLY1305",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equation_EverCrypt.AEAD.key_offset",
"equation_FStar.Integers.int_t", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt128.n", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.uint_t",
"equation_Prims.nat", "equation_Spec.AEAD.ekv_length",
"equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.supported_alg",
"equation_Spec.Poly1305.size_key",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"refinement_interpretation_Tm_refine_f81d6b2edfdc49652737b8dcb0bb4167",
"typing_FStar.UInt.fits", "typing_FStar.UInt128.n",
"typing_FStar.UInt32.add", "typing_FStar.UInt32.v",
"typing_Spec.AEAD.is_supported_alg", "typing_Spec.Poly1305.size_key"
],
0,
"f7d31bf79755d966b20e703374383f8f"
],
[
"EverCrypt.AEAD.aes_gcm_key_expansion",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
"bool_inversion", "constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Prims.unit",
"constructor_distinct_Spec.AEAD.AES128_GCM",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"constructor_distinct_Vale.AES.AES_s.algorithm",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_GCM",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equation_EverCrypt.AEAD.aes_gcm_alg",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Lib.IntTypes.pub_int_t",
"equation_Spec.AEAD.vale_alg_of_alg",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_6410bcec328fc85ed732997cdac8dc2f",
"refinement_interpretation_Tm_refine_703f66a7c02f9a98bc52781f977506bd",
"refinement_interpretation_Tm_refine_a42d5d2af87103782bd6eab813cd1003",
"refinement_interpretation_Tm_refine_d1d6c7c0391d4d930ecf96472414a2d3",
"typing_Spec.AEAD.vale_alg_of_alg",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled", "unit_typing"
],
0,
"a13bfdc7db5626a250b4ff5ff3b3817b"
],
[
"EverCrypt.AEAD.aes_gcm_keyhash_init",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
"bool_inversion", "constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Prims.unit",
"constructor_distinct_Spec.AEAD.AES128_GCM",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"constructor_distinct_Vale.AES.AES_s.algorithm",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_GCM",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equation_EverCrypt.AEAD.aes_gcm_alg",
"equation_FStar.Integers.int_t",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Lib.IntTypes.pub_int_t",
"equation_Spec.AEAD.vale_alg_of_alg",
"equation_Vale.Def.Words_s.nat32",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_3224d6c046f6c42e4ca150f2ed1420f0",
"refinement_interpretation_Tm_refine_6d25514c221d437c17bb43f9bf8b91da",
"refinement_interpretation_Tm_refine_703f66a7c02f9a98bc52781f977506bd",
"refinement_interpretation_Tm_refine_de9dc00542515f2d45f6d8c68f806cc9",
"typing_Spec.AEAD.vale_alg_of_alg",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled", "unit_typing"
],
0,
"efe4b4f7fa5d3ee67abe6babd283822f"
],
[
"EverCrypt.AEAD.impl_of_aes_gcm_alg",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.AEAD.AES128_GCM",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_GCM",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equation_EverCrypt.AEAD.aes_gcm_alg",
"refinement_interpretation_Tm_refine_703f66a7c02f9a98bc52781f977506bd"
],
0,
"79c10e534fc5f5d46b23338f556cf482"
],
[
"EverCrypt.AEAD.create_in_aes_gcm",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Def.Words.Seq_s_interpretation_Tm_arrow_49e1bcc308a31329f00baed943b7728c",
"Vale.Def.Words.Seq_s_interpretation_Tm_arrow_b5c4f50444ae2910f46fcd2f48e0605f",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_EverCrypt.AEAD.Vale_AES128_GCM",
"constructor_distinct_EverCrypt.AEAD.Vale_AES256_GCM",
"constructor_distinct_EverCrypt.Error.Success",
"constructor_distinct_EverCrypt.Error.UnsupportedAlgorithm",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AEAD.AES128_GCM",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "eq2-interp",
"equality_tok_EverCrypt.AEAD.Vale_AES128_GCM@tok",
"equality_tok_EverCrypt.AEAD.Vale_AES256_GCM@tok",
"equality_tok_EverCrypt.Error.Success@tok",
"equality_tok_EverCrypt.Error.UnsupportedAlgorithm@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equation_EverCrypt.AEAD.aes_gcm_alg",
"equation_EverCrypt.AEAD.as_kv", "equation_EverCrypt.AEAD.ekv_len",
"equation_EverCrypt.AEAD.footprint",
"equation_EverCrypt.AEAD.footprint_s",
"equation_EverCrypt.AEAD.freeable",
"equation_EverCrypt.AEAD.freeable_s",
"equation_EverCrypt.AEAD.impl_of_aes_gcm_alg",
"equation_EverCrypt.AEAD.invariant",
"equation_EverCrypt.AEAD.invariant_s",
"equation_EverCrypt.AEAD.key_offset",
"equation_EverCrypt.AEAD.state", "equation_EverCrypt.Hash.fresh_loc",
"equation_EverCrypt.Hash.loc_in",
"equation_EverCrypt.Hash.loc_unused_in",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Integers.v",
"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.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt128.n", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.pointer_or_null",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.l_True", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AEAD.ekv",
"equation_Spec.AEAD.ekv_length", "equation_Spec.AEAD.expand",
"equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.key_length", "equation_Spec.AEAD.lbytes",
"equation_Spec.AEAD.vale_alg_of_alg",
"equation_Spec.Poly1305.size_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.AES_s.key_to_round_keys_LE",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"equation_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing",
"interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
"kinding_EverCrypt.AEAD.state_s@tok",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_EverCrypt.AEAD.invariant_loc_in_footprint",
"lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_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_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_addr_gsub",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.frameOf_gsub",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_addresses_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_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",
"lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_uint8_to_seq_nat8",
"partial_app_typing_d34566d6a1164955778f9afb3b992ec3",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.AEAD.Ek_ek",
"projection_inverse_EverCrypt.AEAD.Ek_impl",
"projection_inverse_EverCrypt.AEAD.Ek_kv",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_0b9523200864b03f5ad9eb51d96a725b",
"refinement_interpretation_Tm_refine_2308e51609e260044ba9287356e3c99b",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_416d0f805341e247c88dc3b5c65a99d4",
"refinement_interpretation_Tm_refine_4b92c12645dc975f1c355e2809aacb84",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_601254ebe274211073b2024a11d02039",
"refinement_interpretation_Tm_refine_6410bcec328fc85ed732997cdac8dc2f",
"refinement_interpretation_Tm_refine_6761149c04877b967d9f292c06a86206",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_703f66a7c02f9a98bc52781f977506bd",
"refinement_interpretation_Tm_refine_8052c4643f51051e2504640bb8316923",
"refinement_interpretation_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
"refinement_interpretation_Tm_refine_8e949bcfbd75e58aef2a3823094035bd",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ab02c6af3f9307692f184b6227f4c573",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_b836d39e81cfc717f7393f7117d32554",
"refinement_interpretation_Tm_refine_b8c10d9d868d2e33eba75ae3c3181c6f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
"typing_EverCrypt.AEAD.key_offset", "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.Seq.Base.create", "typing_FStar.Seq.Base.init",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.seq",
"typing_FStar.Set.singleton", "typing_FStar.UInt.fits",
"typing_FStar.UInt128.n", "typing_FStar.UInt32.add",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
"typing_LowStar.Buffer.pointer_or_null",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_LowStar.Monotonic.Buffer.loc_unused_in", "typing_Prims.pow2",
"typing_Spec.AEAD.kv", "typing_Spec.Poly1305.size_key",
"typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
"typing_Tm_abs_86c482bea7f4b3e185db7eb456de0b9f",
"typing_Vale.AES.AES_s.aes_encrypt_LE_def",
"typing_Vale.AES.AES_s.key_to_round_keys_LE",
"typing_Vale.AES.OptPublic.get_hkeys_reqs",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"typing_Vale.Lib.Seqs_s.seq_map",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_tok_EverCrypt.Error.Success@tok",
"typing_tok_EverCrypt.Error.UnsupportedAlgorithm@tok",
"typing_tok_Spec.AEAD.AES256_GCM@tok",
"typing_tok_Vale.AES.AES_s.AES_128@tok",
"typing_tok_Vale.AES.AES_s.AES_256@tok"
],
0,
"0dc7d9aa28bfdbe8ec3210b394689396"
],
[
"EverCrypt.AEAD.create_in",
1,
0,
0,
[ "@query" ],
0,
"8fc8ea8321ebd71f8e2a06ac2f1fa145"
],
[
"EverCrypt.AEAD.create_in",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_EverCrypt.Error.UnsupportedAlgorithm",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_GCM",
"disc_equation_Spec.AEAD.CHACHA20_POLY1305",
"equality_tok_EverCrypt.Error.UnsupportedAlgorithm@tok",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equality_tok_Spec.AEAD.CHACHA20_POLY1305@tok",
"equation_FStar.HyperStack.ST.equal_stack_domains",
"equation_FStar.HyperStack.ST.is_eternal_region",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperStack.is_eternal_color",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Lib.IntTypes.pub_int_t",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2308e51609e260044ba9287356e3c99b",
"refinement_interpretation_Tm_refine_a681e857996070b6bb92b15cac23f97c",
"refinement_interpretation_Tm_refine_b8c10d9d868d2e33eba75ae3c3181c6f",
"refinement_interpretation_Tm_refine_d012dab0de58c3a4f49165e33cd81f6a",
"refinement_interpretation_Tm_refine_d185726290ef4a05a84e06a1667d858d",
"typing_FStar.Monotonic.HyperHeap.color",
"typing_FStar.Monotonic.HyperStack.is_eternal_color",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_tok_EverCrypt.Error.UnsupportedAlgorithm@tok"
],
0,
"5c67ca98a9233d2dfb52937feaf4fc5d"
],
[
"EverCrypt.AEAD.iv_p",
1,
0,
0,
[ "@query" ],
0,
"148b6931f2e5303fd4a708f05df902d2"
],
[
"EverCrypt.AEAD.encrypt_st",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "disc_equation_EverCrypt.AEAD.Failure",
"disc_equation_EverCrypt.AEAD.InvalidKey",
"disc_equation_EverCrypt.AEAD.Success",
"equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.iv_p",
"equation_EverCrypt.AEAD.kv_or_dummy",
"equation_EverCrypt.AEAD.plain_p", "equation_FStar.Integers.v",
"equation_FStar.Pervasives.inversion", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.supported_alg",
"fuel_guarded_inversion_EverCrypt.AEAD.error_code",
"fuel_guarded_inversion_EverCrypt.AEAD.expanded_key",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"inversion-interp", "lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_EverCrypt.AEAD.EK_kv",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_96e95adc5dd2b841bfab679eafa25477",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"refinement_interpretation_Tm_refine_e745cd4c837adb6286b5e82b8d8a6f93",
"typing_EverCrypt.AEAD.__proj__EK__item__kv",
"typing_EverCrypt.AEAD.kv_or_dummy", "typing_FStar.Ghost.reveal",
"typing_LowStar.Buffer.trivial_preorder",
"typing_Spec.AEAD.is_supported_alg"
],
0,
"6c877d0d0031a1080f031a1f21f6c385"
],
[
"EverCrypt.AEAD.aes_gcm_encrypt",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
"bool_inversion", "constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Prims.unit",
"constructor_distinct_Spec.AEAD.AES128_GCM",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"constructor_distinct_Vale.AES.AES_s.algorithm",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_GCM",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equation_EverCrypt.AEAD.aes_gcm_alg",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Lib.IntTypes.pub_int_t",
"equation_Spec.AEAD.vale_alg_of_alg",
"equation_Vale.Def.Words_s.nat32",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_42bcd291350d5dc1a65c7d1903682cee",
"refinement_interpretation_Tm_refine_703f66a7c02f9a98bc52781f977506bd",
"refinement_interpretation_Tm_refine_b839b8b2bbf156035a230ae0e5ff9510",
"refinement_interpretation_Tm_refine_d4074d2af554a77bbc68b03a5f62075d",
"typing_Spec.AEAD.vale_alg_of_alg",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled", "unit_typing"
],
0,
"ffd47be33384124ae63ef36ce73a52c7"
],
[
"EverCrypt.AEAD.encrypt_aes_gcm",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
"Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Def.Words.Seq_s_interpretation_Tm_arrow_49e1bcc308a31329f00baed943b7728c",
"Vale.Def.Words.Seq_s_interpretation_Tm_arrow_b5c4f50444ae2910f46fcd2f48e0605f",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_EverCrypt.Error.InvalidKey",
"constructor_distinct_EverCrypt.Error.Success",
"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_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.AEAD.AES128_GCM",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"constructor_distinct_Spec.AEAD.CHACHA20_POLY1305",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "eq2-interp",
"equality_tok_EverCrypt.Error.InvalidKey@tok",
"equality_tok_EverCrypt.Error.Success@tok",
"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_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equality_tok_Spec.AEAD.CHACHA20_POLY1305@tok",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equation_EverCrypt.AEAD.ad_p",
"equation_EverCrypt.AEAD.aes_gcm_alg",
"equation_EverCrypt.AEAD.as_kv", "equation_EverCrypt.AEAD.footprint",
"equation_EverCrypt.AEAD.footprint_s",
"equation_EverCrypt.AEAD.invariant",
"equation_EverCrypt.AEAD.invariant_s",
"equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.key_offset",
"equation_EverCrypt.AEAD.plain_p", "equation_EverCrypt.AEAD.state",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
"equation_FStar.Integers.v",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_stack_region",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt128.n", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.pointer_or_null",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.l_True", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AEAD.ekv",
"equation_Spec.AEAD.ekv_length", "equation_Spec.AEAD.encrypt",
"equation_Spec.AEAD.expand", "equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.iv_length", "equation_Spec.AEAD.key_length",
"equation_Spec.AEAD.kv", "equation_Spec.AEAD.lbytes",
"equation_Spec.AEAD.max_length", "equation_Spec.AEAD.supported_alg",
"equation_Spec.AEAD.tag_length",
"equation_Spec.AEAD.vale_alg_of_alg",
"equation_Spec.Chacha20.size_nonce",
"equation_Spec.Chacha20Poly1305.size_nonce",
"equation_Spec.Poly1305.size_key",
"equation_Vale.AES.AES_s.is_aes_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.AES_s.key_to_round_keys_LE",
"equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"equation_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.Wrapper.X64.GCMencryptOpt.disjoint_or_eq",
"function_token_typing_FStar.Integers.uint_8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_FStar.UInt8.v",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_LowStar.Monotonic.Buffer.loc_union",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing",
"interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
"interpretation_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
"kinding_EverCrypt.AEAD.state_s@tok",
"kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd1",
"lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Map.lemma_equal_elim",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv", "lemma_FStar.UInt8.vu_inv",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_addr_gsub",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.frameOf_gsub",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.live_is_null",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.Def.Words.Seq.seq_nat32_to_seq_nat8_to_seq_nat32_LE",
"lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_uint8_to_seq_nat8",
"lemma_Vale.Def.Words.Seq.seq_uint8_to_seq_nat8_to_seq_uint8",
"partial_app_typing_d34566d6a1164955778f9afb3b992ec3",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.AEAD.Ek_ek",
"projection_inverse_EverCrypt.AEAD.Ek_kv",
"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",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_22871ed0ff70fd094ad3e8d742624d47",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_416d0f805341e247c88dc3b5c65a99d4",
"refinement_interpretation_Tm_refine_4b807a66ccc2c78e888ecc503feb847b",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_652c28865c9a77f173ebbb63d1c064bd",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_703f66a7c02f9a98bc52781f977506bd",
"refinement_interpretation_Tm_refine_8546ca0b52d966a3f4e536d7dfa1ad3b",
"refinement_interpretation_Tm_refine_8e949bcfbd75e58aef2a3823094035bd",
"refinement_interpretation_Tm_refine_93bc24ed942206d1181ac6f9494a0683",
"refinement_interpretation_Tm_refine_969e1c213781a3f92fbceb3ec89b17a5",
"refinement_interpretation_Tm_refine_96e95adc5dd2b841bfab679eafa25477",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_b836d39e81cfc717f7393f7117d32554",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_c43881637fea8b5528f4439c75737f91",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"refinement_interpretation_Tm_refine_e30a35a28a0ac00b82a8ffa04337da0b",
"refinement_interpretation_Tm_refine_e745cd4c837adb6286b5e82b8d8a6f93",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f5bd462c110c7929d12a73ddb823e022",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
"typing_EverCrypt.AEAD.footprint",
"typing_EverCrypt.AEAD.footprint_s",
"typing_EverCrypt.AEAD.key_offset",
"typing_FStar.Int.Cast.uint32_to_uint64",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Map.sel",
"typing_FStar.Map.upd", "typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.is_stack_region",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.seq", "typing_FStar.Set.complement",
"typing_FStar.Set.mem", "typing_FStar.Set.singleton",
"typing_FStar.Set.union", "typing_FStar.UInt.fits",
"typing_FStar.UInt128.n", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_FStar.UInt8.uint_to_t",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union", "typing_Prims.pow2",
"typing_Spec.AEAD.expand", "typing_Spec.Chacha20.size_nonce",
"typing_Spec.Chacha20Poly1305.size_nonce",
"typing_Spec.Poly1305.size_key",
"typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
"typing_Tm_abs_86c482bea7f4b3e185db7eb456de0b9f",
"typing_Vale.AES.AES_s.aes_encrypt_LE_def",
"typing_Vale.AES.AES_s.key_to_round_keys_LE",
"typing_Vale.AES.OptPublic.get_hkeys_reqs",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.Def.Types_s.quad32",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"typing_Vale.Lib.Seqs_s.seq_map",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled",
"typing_tok_EverCrypt.Error.InvalidKey@tok",
"typing_tok_EverCrypt.Error.Success@tok",
"typing_tok_Spec.AEAD.AES128_GCM@tok",
"typing_tok_Spec.AEAD.AES256_GCM@tok",
"typing_tok_Vale.AES.AES_s.AES_128@tok",
"typing_tok_Vale.AES.AES_s.AES_256@tok"
],
0,
"11de42ba65685f377bb0d320f1d8dc60"
],
[
"EverCrypt.AEAD.encrypt_aes128_gcm",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.AEAD.AES128_GCM",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equation_Spec.AEAD.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"127da8a8410fd7826dcf524a7fd15d3d"
],
[
"EverCrypt.AEAD.encrypt_aes256_gcm",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.AEAD.AES256_GCM",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equation_Spec.AEAD.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"51c4b37a94debaee210c420d654fc03f"
],
[
"EverCrypt.AEAD.encrypt",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "disc_equation_EverCrypt.AEAD.Failure",
"disc_equation_EverCrypt.AEAD.InvalidKey",
"disc_equation_EverCrypt.AEAD.Success",
"equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.iv_p",
"equation_EverCrypt.AEAD.kv_or_dummy",
"equation_EverCrypt.AEAD.plain_p", "equation_FStar.Integers.v",
"equation_FStar.Pervasives.inversion", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.supported_alg",
"fuel_guarded_inversion_EverCrypt.AEAD.error_code",
"fuel_guarded_inversion_EverCrypt.AEAD.expanded_key",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"inversion-interp", "lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_EverCrypt.AEAD.EK_kv",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_96e95adc5dd2b841bfab679eafa25477",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"refinement_interpretation_Tm_refine_e745cd4c837adb6286b5e82b8d8a6f93",
"typing_EverCrypt.AEAD.__proj__EK__item__kv",
"typing_EverCrypt.AEAD.kv_or_dummy", "typing_FStar.Ghost.reveal",
"typing_LowStar.Buffer.trivial_preorder",
"typing_Spec.AEAD.is_supported_alg"
],
0,
"d7eac2eedbeb643d8b0999c3d0f64d27"
],
[
"EverCrypt.AEAD.encrypt",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "constructor_distinct_EverCrypt.Error.InvalidKey",
"constructor_distinct_EverCrypt.Error.Success",
"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_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AEAD.CHACHA20_POLY1305",
"disc_equation_EverCrypt.AEAD.Hacl_CHACHA20_POLY1305",
"disc_equation_EverCrypt.AEAD.Vale_AES128_GCM",
"disc_equation_EverCrypt.AEAD.Vale_AES256_GCM",
"equality_tok_EverCrypt.Error.InvalidKey@tok",
"equality_tok_EverCrypt.Error.Success@tok",
"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_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AEAD.CHACHA20_POLY1305@tok",
"equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.as_kv",
"equation_EverCrypt.AEAD.footprint",
"equation_EverCrypt.AEAD.footprint_s",
"equation_EverCrypt.AEAD.invariant",
"equation_EverCrypt.AEAD.invariant_s",
"equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.plain_p",
"equation_FStar.Integers.v",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Pervasives.inversion", "equation_FStar.UInt.max_int",
"equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.eq_or_disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer_or_null",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AEAD.ad",
"equation_Spec.AEAD.cipher", "equation_Spec.AEAD.cipher_length",
"equation_Spec.AEAD.ekv", "equation_Spec.AEAD.ekv_length",
"equation_Spec.AEAD.encrypt", "equation_Spec.AEAD.encrypted",
"equation_Spec.AEAD.expand", "equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.iv", "equation_Spec.AEAD.iv_length",
"equation_Spec.AEAD.key_length", "equation_Spec.AEAD.kv",
"equation_Spec.AEAD.lbytes", "equation_Spec.AEAD.max_length",
"equation_Spec.AEAD.plain", "equation_Spec.AEAD.supported_alg",
"equation_Spec.AEAD.tag_length", "equation_Spec.Chacha20.size_nonce",
"equation_Spec.Chacha20Poly1305.nonce",
"equation_Spec.Chacha20Poly1305.size_nonce",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"fuel_guarded_inversion_EverCrypt.AEAD.impl",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_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.AEAD.state_s@tok",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.uv_inv", "lemma_Lib.IntTypes.pow2_values",
"lemma_Lib.Sequence.eq_elim",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.live_is_null",
"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_refl",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.AEAD.Ek_ek",
"projection_inverse_EverCrypt.AEAD.Ek_impl",
"projection_inverse_EverCrypt.AEAD.Ek_kv",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_09f10c54cc48f71eb6701e2f2e721a1f",
"refinement_interpretation_Tm_refine_0a44a9c52461f7b29dab1fe1db7afc62",
"refinement_interpretation_Tm_refine_2113892d55dcfb21038c9cc80ff21bea",
"refinement_interpretation_Tm_refine_238c0756014f16e81289c34e231de3b4",
"refinement_interpretation_Tm_refine_2bc44fc2dddd0108edaa155d75f9c5cf",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_58bdadcafa8f630c763ed0b3175cbb75",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_652c28865c9a77f173ebbb63d1c064bd",
"refinement_interpretation_Tm_refine_67a684ae2cdcea98c0a7a1a09bcb3247",
"refinement_interpretation_Tm_refine_7001d717117afb7669cd45b51ad3dc27",
"refinement_interpretation_Tm_refine_93bc24ed942206d1181ac6f9494a0683",
"refinement_interpretation_Tm_refine_96e95adc5dd2b841bfab679eafa25477",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_bc9390aeabb7bbdf9992e75da50293a9",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_cd8943ee2044f75c797c0465a2482c5a",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_e745cd4c837adb6286b5e82b8d8a6f93",
"refinement_interpretation_Tm_refine_ec0e50a60589787896efd904cfd70802",
"refinement_interpretation_Tm_refine_fb77d4109290540100357b20e0a78486",
"refinement_kinding_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"typing_EverCrypt.AEAD.as_kv", "typing_EverCrypt.AEAD.footprint_s",
"typing_FStar.Ghost.reveal", "typing_FStar.Seq.Base.append",
"typing_FStar.Seq.Base.length", "typing_FStar.Set.singleton",
"typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.loc",
"typing_Lib.Sequence.concat",
"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.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_Spec.AEAD.encrypt", "typing_Spec.AEAD.expand",
"typing_Spec.AEAD.is_supported_alg", "typing_Spec.AEAD.kv",
"typing_Spec.Poly1305.size_key",
"typing_tok_EverCrypt.Error.InvalidKey@tok",
"typing_tok_EverCrypt.Error.Success@tok",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"d2d39bc03db4a9a65716cf6bf2b742d8"
],
[
"EverCrypt.AEAD.decrypt_st",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Winfinite",
"disc_equation_EverCrypt.AEAD.Failure",
"disc_equation_EverCrypt.AEAD.InvalidKey",
"disc_equation_EverCrypt.AEAD.Success",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.cipher_p",
"equation_EverCrypt.AEAD.iv_p",
"equation_EverCrypt.AEAD.kv_or_dummy",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.v",
"equation_FStar.Pervasives.inversion", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.supported_alg",
"fuel_guarded_inversion_EverCrypt.AEAD.error_code",
"fuel_guarded_inversion_EverCrypt.AEAD.expanded_key",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"inversion-interp", "lemma_FStar.Seq.Base.lemma_len_append",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_488b4da67cbd9ff7df54538d061a4f05",
"refinement_interpretation_Tm_refine_96e95adc5dd2b841bfab679eafa25477",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"refinement_interpretation_Tm_refine_e30a35a28a0ac00b82a8ffa04337da0b",
"refinement_interpretation_Tm_refine_e745cd4c837adb6286b5e82b8d8a6f93",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_Spec.AEAD.is_supported_alg"
],
0,
"56ded9cbe8d670262be9ff9cddbcf518"
],
[
"EverCrypt.AEAD.aes_gcm_decrypt",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
"bool_inversion", "constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Prims.unit",
"constructor_distinct_Spec.AEAD.AES128_GCM",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"constructor_distinct_Vale.AES.AES_s.algorithm",
"disc_equation_Spec.AEAD.AES128_GCM",
"disc_equation_Spec.AEAD.AES256_GCM",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equation_EverCrypt.AEAD.aes_gcm_alg",
"equation_FStar.Integers.int_t",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Lib.IntTypes.pub_int_t",
"equation_Spec.AEAD.vale_alg_of_alg",
"equation_Vale.Def.Words_s.nat32",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_1cdc487905fc8507a8aceac84f10b7ee",
"refinement_interpretation_Tm_refine_703f66a7c02f9a98bc52781f977506bd",
"refinement_interpretation_Tm_refine_9075ede359e24c550a758570389c9e96",
"refinement_interpretation_Tm_refine_a2fc83624f1fe37dfb2a048fe10e347c",
"typing_Spec.AEAD.vale_alg_of_alg",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.pclmulqdq_enabled", "unit_typing"
],
0,
"03f21a76a12cf03c56c679fa6c523bdf"
],
[
"EverCrypt.AEAD.decrypt_aes_gcm",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Vale.Def.Words.Seq_s_interpretation_Tm_arrow_49e1bcc308a31329f00baed943b7728c",
"Vale.Def.Words.Seq_s_interpretation_Tm_arrow_b5c4f50444ae2910f46fcd2f48e0605f",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def",
"assumption_FStar.UInt64.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing",
"constructor_distinct_EverCrypt.Error.AuthenticationFailure",
"constructor_distinct_EverCrypt.Error.InvalidKey",
"constructor_distinct_EverCrypt.Error.Success",
"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.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"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.AEAD.AES128_GCM",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"constructor_distinct_Spec.AEAD.CHACHA20_POLY1305",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some", "eq2-interp",
"equality_tok_EverCrypt.Error.AuthenticationFailure@tok",
"equality_tok_EverCrypt.Error.InvalidKey@tok",
"equality_tok_EverCrypt.Error.Success@tok",
"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_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equality_tok_Spec.AEAD.CHACHA20_POLY1305@tok",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equation_EverCrypt.AEAD.ad_p",
"equation_EverCrypt.AEAD.aes_gcm_alg",
"equation_EverCrypt.AEAD.as_kv", "equation_EverCrypt.AEAD.cipher_p",
"equation_EverCrypt.AEAD.footprint",
"equation_EverCrypt.AEAD.footprint_s",
"equation_EverCrypt.AEAD.invariant",
"equation_EverCrypt.AEAD.invariant_s",
"equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.key_offset",
"equation_EverCrypt.AEAD.state",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Integers.int", "equation_FStar.Integers.int_t",
"equation_FStar.Integers.nat", "equation_FStar.Integers.uint_8",
"equation_FStar.Integers.v",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_stack_region",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.Pervasives.inversion",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt128.n", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.pointer_or_null",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.l_True", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.AEAD.decrypt", "equation_Spec.AEAD.decrypted",
"equation_Spec.AEAD.ekv", "equation_Spec.AEAD.ekv_length",
"equation_Spec.AEAD.expand", "equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.iv_length", "equation_Spec.AEAD.key_length",
"equation_Spec.AEAD.kv", "equation_Spec.AEAD.lbytes",
"equation_Spec.AEAD.max_length", "equation_Spec.AEAD.supported_alg",
"equation_Spec.AEAD.tag_length",
"equation_Spec.AEAD.vale_alg_of_alg",
"equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_nonce",
"equation_Spec.Chacha20Poly1305.size_nonce",
"equation_Spec.Poly1305.size_key",
"equation_Vale.AES.AES_s.is_aes_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.AES_s.key_to_round_keys_LE",
"equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"equation_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.Wrapper.X64.GCMdecryptOpt.disjoint_or_eq",
"fuel_guarded_inversion_EverCrypt.AEAD.impl",
"function_token_typing_FStar.Integers.uint_8",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_FStar.UInt8.v",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing",
"interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
"interpretation_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
"inversion-interp", "kinding_EverCrypt.AEAD.state_s@tok",
"kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd1",
"lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv", "lemma_FStar.UInt64.uv_inv",
"lemma_FStar.UInt64.vu_inv", "lemma_FStar.UInt8.vu_inv",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_addr_gsub",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.frameOf_gsub",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.live_is_null",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"lemma_Vale.Def.Words.Seq.seq_nat32_to_seq_nat8_to_seq_nat32_LE",
"lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_uint8_to_seq_nat8",
"lemma_Vale.Def.Words.Seq.seq_uint8_to_seq_nat8_to_seq_uint8",
"partial_app_typing_d34566d6a1164955778f9afb3b992ec3",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"proj_equation_FStar.Pervasives.Native.Some_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.AEAD.Ek_ek",
"projection_inverse_EverCrypt.AEAD.Ek_impl",
"projection_inverse_EverCrypt.AEAD.Ek_kv",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_106d359244143316cc15c6e37cc7caeb",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_22871ed0ff70fd094ad3e8d742624d47",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_40c6f008a3f2c9d3927b30ab6308c9a2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_416d0f805341e247c88dc3b5c65a99d4",
"refinement_interpretation_Tm_refine_488b4da67cbd9ff7df54538d061a4f05",
"refinement_interpretation_Tm_refine_4b807a66ccc2c78e888ecc503feb847b",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_652c28865c9a77f173ebbb63d1c064bd",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_703f66a7c02f9a98bc52781f977506bd",
"refinement_interpretation_Tm_refine_8a88f84ddb86f6a45826b1d92939a27c",
"refinement_interpretation_Tm_refine_8e949bcfbd75e58aef2a3823094035bd",
"refinement_interpretation_Tm_refine_93bc24ed942206d1181ac6f9494a0683",
"refinement_interpretation_Tm_refine_96e95adc5dd2b841bfab679eafa25477",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_b836d39e81cfc717f7393f7117d32554",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_c43881637fea8b5528f4439c75737f91",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"refinement_interpretation_Tm_refine_e30a35a28a0ac00b82a8ffa04337da0b",
"refinement_interpretation_Tm_refine_e745cd4c837adb6286b5e82b8d8a6f93",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
"typing_EverCrypt.AEAD.footprint",
"typing_EverCrypt.AEAD.footprint_s",
"typing_EverCrypt.AEAD.key_offset",
"typing_FStar.Int.Cast.uint32_to_uint64",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Map.sel",
"typing_FStar.Map.upd", "typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.is_stack_region",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.seq", "typing_FStar.Seq.Base.slice",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_FStar.UInt.fits", "typing_FStar.UInt128.n",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
"typing_FStar.UInt8.uint_to_t",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union", "typing_Prims.pow2",
"typing_Spec.AEAD.expand", "typing_Spec.AEAD.tag_length",
"typing_Spec.Chacha20.size_block", "typing_Spec.Chacha20.size_nonce",
"typing_Spec.Chacha20Poly1305.size_nonce",
"typing_Spec.Poly1305.size_key",
"typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
"typing_Tm_abs_86c482bea7f4b3e185db7eb456de0b9f",
"typing_Vale.AES.AES_s.aes_encrypt_LE_def",
"typing_Vale.AES.AES_s.key_to_round_keys_LE",
"typing_Vale.AES.OptPublic.get_hkeys_reqs",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.Def.Types_s.quad32",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8",
"typing_Vale.Interop.Assumptions.win",
"typing_Vale.Lib.Seqs_s.seq_map",
"typing_tok_EverCrypt.Error.AuthenticationFailure@tok",
"typing_tok_EverCrypt.Error.InvalidKey@tok",
"typing_tok_EverCrypt.Error.Success@tok",
"typing_tok_Spec.AEAD.AES128_GCM@tok",
"typing_tok_Spec.AEAD.AES256_GCM@tok",
"typing_tok_Vale.AES.AES_s.AES_128@tok",
"typing_tok_Vale.AES.AES_s.AES_256@tok"
],
0,
"8339bccdf32b971afda5276963d9c7dd"
],
[
"EverCrypt.AEAD.decrypt_aes128_gcm",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.AEAD.AES128_GCM",
"equality_tok_Spec.AEAD.AES128_GCM@tok",
"equation_Spec.AEAD.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"356e21b03a045482705c692cb84c650b"
],
[
"EverCrypt.AEAD.decrypt_aes256_gcm",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.AEAD.AES256_GCM",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equation_Spec.AEAD.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"e262ea70dd417d673ca8943f5f6669c4"
],
[
"EverCrypt.AEAD.decrypt",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Winfinite",
"disc_equation_EverCrypt.AEAD.Failure",
"disc_equation_EverCrypt.AEAD.InvalidKey",
"disc_equation_EverCrypt.AEAD.Success",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.cipher_p",
"equation_EverCrypt.AEAD.iv_p",
"equation_EverCrypt.AEAD.kv_or_dummy",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.v",
"equation_FStar.Pervasives.inversion", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.supported_alg",
"fuel_guarded_inversion_EverCrypt.AEAD.error_code",
"fuel_guarded_inversion_EverCrypt.AEAD.expanded_key",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"inversion-interp", "lemma_FStar.Seq.Base.lemma_len_append",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_488b4da67cbd9ff7df54538d061a4f05",
"refinement_interpretation_Tm_refine_96e95adc5dd2b841bfab679eafa25477",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"refinement_interpretation_Tm_refine_e30a35a28a0ac00b82a8ffa04337da0b",
"refinement_interpretation_Tm_refine_e745cd4c837adb6286b5e82b8d8a6f93",
"typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_Spec.AEAD.is_supported_alg"
],
0,
"d5fc6c911088f46b7607b10bd36adbfb"
],
[
"EverCrypt.AEAD.decrypt",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing",
"constructor_distinct_EverCrypt.Error.AuthenticationFailure",
"constructor_distinct_EverCrypt.Error.InvalidKey",
"constructor_distinct_EverCrypt.Error.Success",
"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_FStar.Pervasives.Native.None",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AEAD.CHACHA20_POLY1305",
"disc_equation_EverCrypt.AEAD.Hacl_CHACHA20_POLY1305",
"disc_equation_EverCrypt.AEAD.Vale_AES128_GCM",
"disc_equation_EverCrypt.AEAD.Vale_AES256_GCM",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_EverCrypt.Error.AuthenticationFailure@tok",
"equality_tok_EverCrypt.Error.InvalidKey@tok",
"equality_tok_EverCrypt.Error.Success@tok",
"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_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AEAD.CHACHA20_POLY1305@tok",
"equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.as_kv",
"equation_EverCrypt.AEAD.cipher_p",
"equation_EverCrypt.AEAD.invariant",
"equation_EverCrypt.AEAD.invariant_s",
"equation_EverCrypt.AEAD.iv_p", "equation_FStar.Integers.v",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Pervasives.inversion", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.eq_or_disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.uint_t",
"equation_Lib.IntTypes.uint_v", "equation_Lib.Sequence.lseq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer_or_null",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.AEAD.decrypt", "equation_Spec.AEAD.ekv",
"equation_Spec.AEAD.ekv_length", "equation_Spec.AEAD.expand",
"equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.iv_length", "equation_Spec.AEAD.lbytes",
"equation_Spec.AEAD.max_length", "equation_Spec.AEAD.supported_alg",
"equation_Spec.AEAD.tag_length",
"equation_Spec.Chacha20Poly1305.aead_decrypt",
"equation_Spec.Chacha20Poly1305.size_block",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"fuel_guarded_inversion_EverCrypt.AEAD.impl",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "inversion-interp",
"kinding_EverCrypt.AEAD.state_s@tok",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.live_is_null",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_FStar.Pervasives.Native.Some_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_EverCrypt.AEAD.Ek_ek",
"projection_inverse_EverCrypt.AEAD.Ek_impl",
"projection_inverse_EverCrypt.AEAD.Ek_kv",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_1cc24a0b07285f69bf5ac5d6da259a9e",
"refinement_interpretation_Tm_refine_2113892d55dcfb21038c9cc80ff21bea",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36c99d2ba59e38e9fbc31051b70e0749",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_40c6f008a3f2c9d3927b30ab6308c9a2",
"refinement_interpretation_Tm_refine_488b4da67cbd9ff7df54538d061a4f05",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_55ebe6b916d93cfa09c5c84d80b64399",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_652c28865c9a77f173ebbb63d1c064bd",
"refinement_interpretation_Tm_refine_73a2255885f724875aa1dd780e3712c6",
"refinement_interpretation_Tm_refine_93bc24ed942206d1181ac6f9494a0683",
"refinement_interpretation_Tm_refine_96e95adc5dd2b841bfab679eafa25477",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"refinement_interpretation_Tm_refine_e745cd4c837adb6286b5e82b8d8a6f93",
"refinement_kinding_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"typing_FStar.Ghost.reveal", "typing_FStar.Seq.Base.append",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt32.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_Spec.AEAD.expand", "typing_Spec.AEAD.is_supported_alg",
"typing_Spec.AEAD.kv", "typing_Spec.Poly1305.size_key",
"typing_tok_EverCrypt.Error.AuthenticationFailure@tok",
"typing_tok_EverCrypt.Error.InvalidKey@tok",
"typing_tok_EverCrypt.Error.Success@tok"
],
0,
"3aa58667804b192e293192d262e390aa"
],
[
"EverCrypt.AEAD.free",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"bool_typing", "equation_EverCrypt.AEAD.footprint",
"equation_EverCrypt.AEAD.footprint_s",
"equation_EverCrypt.AEAD.freeable",
"equation_EverCrypt.AEAD.freeable_s",
"equation_EverCrypt.AEAD.invariant",
"equation_EverCrypt.AEAD.invariant_s",
"equation_EverCrypt.AEAD.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_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AEAD.supported_alg",
"function_token_typing_FStar.Monotonic.Heap.heap",
"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",
"kinding_EverCrypt.AEAD.state_s@tok",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.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.AEAD.Ek_ek",
"refinement_interpretation_Tm_refine_23be030692bc555feafbdc4fa2251593",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_ada1da73f5ce82a6efdf946ba47c1752",
"refinement_interpretation_Tm_refine_aec39ec305a10defb4b74d242f75f39d",
"refinement_interpretation_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"refinement_kinding_Tm_refine_d2d399e4b0cd736cb6130361c7530aa2",
"typing_EverCrypt.AEAD.footprint",
"typing_EverCrypt.AEAD.footprint_s", "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_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,
"1018d8f90fb67f59aec47cb7383125dc"
]
]
]
Computing file changes ...
