[ "(6³^iÜþßL´Ãy~7K ", [ [ "EverCrypt.AEAD.uu___0", 1, 0, 0, [ "@query" ], 0, "65b415da2a77862ca96b0d639e070e2d" ], [ "EverCrypt.AEAD.supported_alg_of_impl", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "disc_equation_Spec.Cipher.Expansion.Hacl_CHACHA20", "disc_equation_Spec.Cipher.Expansion.Vale_AES128", "disc_equation_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equation_Lib.IntTypes.unsigned", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Cipher.Expansion.uu___30", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Cipher.Expansion.impl", "function_token_typing_Spec.Cipher.Expansion.uu___30", "inversion-interp", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.is_supported_alg", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Spec.Agile.AEAD.AES256_GCM@tok" ], 0, "9d1e885431701634c793364f61cefda4" ], [ "EverCrypt.AEAD.alg_of_vale_impl", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Spec.Cipher.Expansion.Hacl_CHACHA20", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "disc_equation_Spec.Cipher.Expansion.Vale_AES128", "disc_equation_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.CTR.Keys.vale_impl", "equation_FStar.Pervasives.inversion", "fuel_guarded_inversion_Spec.Cipher.Expansion.impl", "inversion-interp", "refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35" ], 0, "f63e0d425b84da0b6f41dc359fd7e10d" ], [ "EverCrypt.AEAD.loc_includes_union_l_footprint_s", 1, 0, 0, [ "@query" ], 0, "ba3a92cd61e4a6eb46034742dba80085" ], [ "EverCrypt.AEAD.invariant_s", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "assumption_Spec.Agile.AEAD.alg__uu___haseq", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.AES.AES128", "constructor_distinct_Spec.AES.AES256", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.Cipher.AES128", "constructor_distinct_Spec.Agile.Cipher.AES256", "constructor_distinct_Spec.Agile.Cipher.CHACHA20", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "disc_equation_Spec.Cipher.Expansion.Hacl_CHACHA20", "disc_equation_Spec.Cipher.Expansion.Vale_AES128", "disc_equation_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.AES.AES128@tok", "equality_tok_Spec.AES.AES256@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.Cipher.AES128@tok", "equality_tok_Spec.Agile.Cipher.AES256@tok", "equality_tok_Spec.Agile.Cipher.CHACHA20@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.AEAD.supported_alg_of_impl", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.aes_key", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.AES.key_size", "equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.kv", "equation_Spec.Agile.AEAD.lbytes", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.Cipher.aes_alg_of_alg", "equation_Spec.Agile.Cipher.key", "equation_Spec.Agile.Cipher.key_length", "equation_Spec.Chacha20.key", "equation_Spec.Chacha20.size_key", "equation_Spec.Cipher.Expansion.cipher_alg_of_impl", "equation_Spec.Cipher.Expansion.concrete_xkey_length", "equation_Spec.Cipher.Expansion.uu___30", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "fuel_guarded_inversion_Spec.Cipher.Expansion.impl", "function_token_typing_Prims.int", "function_token_typing_Spec.Cipher.Expansion.uu___30", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "inversion-interp", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_982fb3d3fec67274e50be352a80fb36e", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.is_supported_alg", "typing_Spec.Cipher.Expansion.concrete_xkey_length", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "cdf5e74300f6a7b2225735549869eb24" ], [ "EverCrypt.AEAD.invariant", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_EverCrypt.AEAD.state", "equation_LowStar.Buffer.pointer", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e" ], 0, "6f3157aa600b7382882155e56305a39a" ], [ "EverCrypt.AEAD.invariant_loc_in_footprint", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "data_elim_EverCrypt.AEAD.Ek", "equality_tok_FStar.Integers.W8@tok", "equation_EverCrypt.AEAD.footprint", "equation_EverCrypt.AEAD.footprint_s", "equation_EverCrypt.AEAD.invariant", "equation_EverCrypt.AEAD.invariant_s", "equation_EverCrypt.AEAD.state", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.loc_in", "equation_Prims.eqtype", "equation_Prims.nat", "fuel_guarded_inversion_EverCrypt.AEAD.state_s", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.UInt8.t", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "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", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "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, "06e3da5e5c964a9dd98fea1caa20948a" ], [ "EverCrypt.AEAD.frame_invariant", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.AES.AES128", "constructor_distinct_Spec.AES.AES256", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.Cipher.AES128", "constructor_distinct_Spec.Agile.Cipher.AES256", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "data_elim_EverCrypt.AEAD.Ek", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.AES.AES128@tok", "equality_tok_Spec.AES.AES256@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.Cipher.AES128@tok", "equality_tok_Spec.Agile.Cipher.AES256@tok", "equation_EverCrypt.AEAD.footprint", "equation_EverCrypt.AEAD.footprint_s", "equation_EverCrypt.AEAD.invariant", "equation_EverCrypt.AEAD.invariant_s", "equation_EverCrypt.AEAD.state", "equation_EverCrypt.AEAD.supported_alg_of_impl", "equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.aes_key", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.AES.key_size", "equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.kv", "equation_Spec.Agile.AEAD.lbytes", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.Cipher.aes_alg_of_alg", "equation_Spec.Agile.Cipher.key", "equation_Spec.Agile.Cipher.key_length", "equation_Spec.Chacha20.size_key", "equation_Spec.Cipher.Expansion.cipher_alg_of_impl", "equation_Spec.Cipher.Expansion.concrete_expand", "equation_Spec.Cipher.Expansion.concrete_xkey", "equation_Spec.Cipher.Expansion.concrete_xkey_length", "equation_Spec.Cipher.Expansion.uu___30", "equation_Spec.Cipher.Expansion.vale_xkey_length", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_EverCrypt.AEAD.state_s", "fuel_guarded_inversion_Spec.Cipher.Expansion.impl", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Prims.int", "function_token_typing_Spec.Cipher.Expansion.uu___30", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "inversion-interp", "kinding_EverCrypt.AEAD.state_s@tok", "lemma_EverCrypt.AEAD.invert_state_s", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "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", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_982fb3d3fec67274e50be352a80fb36e", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.AEAD.footprint_s", "typing_FStar.Ghost.reveal", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.get", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.mgsub", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.is_supported_alg", "typing_Spec.Agile.AEAD.kv", "typing_Spec.Cipher.Expansion.concrete_expand", "typing_Spec.Cipher.Expansion.concrete_xkey_length", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "ad438483988759d7cd369f492ce09b2d" ], [ "EverCrypt.AEAD.alg_of_state", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Spec.Cipher.Expansion.Hacl_CHACHA20", "disc_equation_Spec.Cipher.Expansion.Vale_AES128", "disc_equation_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equation_EverCrypt.AEAD.invariant", "equation_EverCrypt.AEAD.invariant_s", "equation_EverCrypt.AEAD.supported_alg_of_impl", "equation_FStar.Pervasives.inversion", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Cipher.Expansion.impl", "inversion-interp", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_EverCrypt.AEAD.Ek_impl", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_c4da9253bc1c72e5c11cb9fcfdcf3b32", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Spec.Agile.AEAD.AES128_GCM@tok", "typing_tok_Spec.Agile.AEAD.AES256_GCM@tok", "typing_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok" ], 0, "6668b1482d12205b13476c8e7c5a85cf" ], [ "EverCrypt.AEAD.create_in_st", 1, 0, 0, [ "@query", "projection_inverse_BoxBool_proj_0" ], 0, "0ba500292108bbfcafca9cfa653b5ada" ], [ "EverCrypt.AEAD.alloca_st", 1, 0, 0, [ "@query" ], 0, "17d3a4c2be10ae04c64678325e9f3ed6" ], [ "EverCrypt.AEAD.create_in_chacha20_poly1305", 1, 0, 0, [ "@query" ], 0, "bd26ba3353363eb091a5e8079f94f184" ], [ "EverCrypt.AEAD.create_in_chacha20_poly1305", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_EverCrypt.Error.Success", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.Cipher.CHACHA20", "constructor_distinct_Spec.Cipher.Expansion.Hacl_CHACHA20", "equality_tok_EverCrypt.Error.Success@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.Cipher.CHACHA20@tok", "equality_tok_Spec.Cipher.Expansion.Hacl_CHACHA20@tok", "equation_EverCrypt.AEAD.as_kv", "equation_EverCrypt.AEAD.config_pre", "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.supported_alg_of_impl", "equation_EverCrypt.CTR.Keys.uint8", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.HyperStack.ST.is_eternal_region", "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.is_heap_color", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "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.fresh_loc", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.Cipher.key_length", "equation_Spec.Chacha20.size_key", "equation_Spec.Cipher.Expansion.concrete_expand", "equation_Spec.Cipher.Expansion.concrete_xkey_length", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "kinding_EverCrypt.AEAD.state_s@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_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_refl", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Seq.Base.lemma_index_upd1", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_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", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_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_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_161e04719814801d293219f408210f95", "refinement_interpretation_Tm_refine_3adad2fa15bf57cd1bb4986f7f40a94b", "refinement_interpretation_Tm_refine_405fda013880964b52cbb5b7111863be", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_984d8cab34fc52b3ffe0c6a5bc4d2090", "refinement_interpretation_Tm_refine_9f148e827f089e37835ae98ab1a7a73a", "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1", "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_da11fddce86d1a8b8207757b4a6e95de", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "true_interp", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.color", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.is_heap_color", "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_Lib.IntTypes.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.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_LowStar.Monotonic.Buffer.loc_unused_in", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.Agile.AEAD.kv", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_EverCrypt.Error.Success@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok" ], 0, "5f4ef4d02989db48f5e3a5b550478b3d" ], [ "EverCrypt.AEAD.create_in_aes_gcm", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_EverCrypt.Error.Success", "constructor_distinct_EverCrypt.Error.UnsupportedAlgorithm", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.AES.AES128", "constructor_distinct_Spec.AES.AES256", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Agile.Cipher.AES128", "constructor_distinct_Spec.Agile.Cipher.AES256", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_EverCrypt.Error.Success@tok", "equality_tok_EverCrypt.Error.UnsupportedAlgorithm@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.AES.AES128@tok", "equality_tok_Spec.AES.AES256@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.Cipher.AES128@tok", "equality_tok_Spec.Agile.Cipher.AES256@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_EverCrypt.AEAD.as_kv", "equation_EverCrypt.AEAD.config_pre", "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.supported_alg_of_impl", "equation_EverCrypt.CTR.Keys.concrete_xkey_len", "equation_EverCrypt.CTR.Keys.uint8", "equation_EverCrypt.CTR.Keys.vale_impl", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Integers.int_t", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_heap_color", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "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.fresh_loc", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.AES.key_size", "equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.Cipher.aes_alg_of_alg", "equation_Spec.Agile.Cipher.key_length", "equation_Spec.Cipher.Expansion.cipher_alg_of_impl", "equation_Spec.Cipher.Expansion.concrete_xkey_length", "equation_Spec.Cipher.Expansion.uu___29", "equation_Spec.Cipher.Expansion.uu___30", "equation_Spec.Cipher.Expansion.vale_xkey_length", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg", "fuel_guarded_inversion_Spec.Cipher.Expansion.impl", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Prims.int", "function_token_typing_Spec.Cipher.Expansion.uu___29", "function_token_typing_Spec.Cipher.Expansion.uu___30", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "inversion-interp", "kinding_EverCrypt.AEAD.state_s@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_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_index_create", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.as_seq_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_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_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", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_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_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_161e04719814801d293219f408210f95", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_33d23738b4b15f7b09fd193199ac0f72", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_67050f0bec933c5477cc1dda6e0b4da0", "refinement_interpretation_Tm_refine_6ea4bc7028499f65caa924b56470ac27", "refinement_interpretation_Tm_refine_709aff84c75b0fff77dcbf3b529649dd", "refinement_interpretation_Tm_refine_8ae37d1557d85b8479513decc054eed2", "refinement_interpretation_Tm_refine_9100ab96093283c751c14419f2de4403", "refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cc39cb5239b79355a7fada467c865a04", "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f1c49255c65b3e9495e71abe5cded67f", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "true_interp", "typing_EverCrypt.AEAD.alg_of_vale_impl", "typing_EverCrypt.CTR.Keys.concrete_xkey_len", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.color", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.is_heap_color", "typing_FStar.Seq.Base.create", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "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_Spec.AES.gf8", "typing_Spec.Agile.AEAD.kv", "typing_Spec.Cipher.Expansion.cipher_alg_of_impl", "typing_Spec.Cipher.Expansion.concrete_xkey_length", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_EverCrypt.Error.Success@tok", "typing_tok_EverCrypt.Error.UnsupportedAlgorithm@tok" ], 0, "1d024d972752d0ff8610a26484b10be1" ], [ "EverCrypt.AEAD.create_in", 1, 0, 0, [ "@query" ], 0, "86e3ed2944b8913daec11cd1f3592e9b" ], [ "EverCrypt.AEAD.create_in", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_EverCrypt.Error.UnsupportedAlgorithm", "disc_equation_Spec.Agile.AEAD.AES128_GCM", "disc_equation_Spec.Agile.AEAD.AES256_GCM", "disc_equation_Spec.Agile.AEAD.CHACHA20_POLY1305", "equality_tok_EverCrypt.Error.UnsupportedAlgorithm@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.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", "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_5cfeaf80ca9486357b6c6d01114a47a0", "refinement_interpretation_Tm_refine_66ea836f4d62f44eace18c4297943b11", "refinement_interpretation_Tm_refine_984d8cab34fc52b3ffe0c6a5bc4d2090", "refinement_interpretation_Tm_refine_e55ca2031f0926499978c5b5c26be0b9", "refinement_interpretation_Tm_refine_e692cabf996d3cca074ab12757df58a8", "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, "79555889392f57d84efb84e1a8b99ec1" ], [ "EverCrypt.AEAD.alloca_chacha20_poly1305", 1, 0, 0, [ "@query" ], 0, "6e5690baadd60fba23bda228e76bf8aa" ], [ "EverCrypt.AEAD.alloca_chacha20_poly1305", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.Cipher.CHACHA20", "constructor_distinct_Spec.Cipher.Expansion.Hacl_CHACHA20", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.Cipher.CHACHA20@tok", "equality_tok_Spec.Cipher.Expansion.Hacl_CHACHA20@tok", "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.supported_alg_of_impl", "equation_EverCrypt.CTR.Keys.uint8", "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.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.Cipher.key_length", "equation_Spec.Chacha20.size_key", "equation_Spec.Cipher.Expansion.concrete_expand", "equation_Spec.Cipher.Expansion.concrete_xkey_length", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "kinding_EverCrypt.AEAD.state_s@tok", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "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_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_addresses_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "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", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "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_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0319fb5ba557ddfef833720396790fd1", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2c00302a4ec68ddf994feab8aa0d428c", "refinement_interpretation_Tm_refine_3adad2fa15bf57cd1bb4986f7f40a94b", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_6c9144323fd28b0cbde669abc7f6d410", "refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "true_interp", "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_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_LowStar.Monotonic.Buffer.loc_unused_in", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.is_supported_alg", "typing_Spec.Agile.AEAD.key_length", "typing_Spec.Agile.AEAD.kv", "typing_Spec.Chacha20.size_key", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok" ], 0, "8e073eb132540481b2f81991a9e7878d" ], [ "EverCrypt.AEAD.alloca_aes_gcm", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "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.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.AES.AES128", "constructor_distinct_Spec.AES.AES256", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Agile.Cipher.AES128", "constructor_distinct_Spec.Agile.Cipher.AES256", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "constructor_distinct_Tm_unit", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.AES.AES128@tok", "equality_tok_Spec.AES.AES256@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.Cipher.AES128@tok", "equality_tok_Spec.Agile.Cipher.AES256@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_EverCrypt.AEAD.as_kv", "equation_EverCrypt.AEAD.config_pre", "equation_EverCrypt.AEAD.footprint", "equation_EverCrypt.AEAD.footprint_s", "equation_EverCrypt.AEAD.invariant", "equation_EverCrypt.AEAD.invariant_s", "equation_EverCrypt.AEAD.supported_alg_of_impl", "equation_EverCrypt.CTR.Keys.concrete_xkey_len", "equation_EverCrypt.CTR.Keys.uint8", "equation_EverCrypt.CTR.Keys.vale_impl", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Integers.int_t", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_stack_region", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.AES.key_size", "equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.AEAD.uu___2", "equation_Spec.Agile.Cipher.aes_alg_of_alg", "equation_Spec.Agile.Cipher.key_length", "equation_Spec.Cipher.Expansion.cipher_alg_of_impl", "equation_Spec.Cipher.Expansion.concrete_xkey_length", "equation_Spec.Cipher.Expansion.uu___29", "equation_Spec.Cipher.Expansion.uu___30", "equation_Spec.Cipher.Expansion.vale_xkey_length", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Spec.Agile.AEAD.alg", "fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg", "fuel_guarded_inversion_Spec.Cipher.Expansion.impl", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "function_token_typing_Spec.Agile.AEAD.uu___2", "function_token_typing_Spec.Cipher.Expansion.uu___29", "function_token_typing_Spec.Cipher.Expansion.uu___30", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "inversion-interp", "kinding_EverCrypt.AEAD.state_s@tok", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_gsub", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_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_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", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_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_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_2d0afb0871a43a7500fee674b7b6e874", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_33d23738b4b15f7b09fd193199ac0f72", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_41e78e7e47a05d17020ec5b142e1d04c", "refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_709aff84c75b0fff77dcbf3b529649dd", "refinement_interpretation_Tm_refine_9100ab96093283c751c14419f2de4403", "refinement_interpretation_Tm_refine_beb7c6d4296d74db0f17e5e149104d65", "refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c4fea1cb1fba11da5838397b5ec2f3e9", "refinement_interpretation_Tm_refine_cc39cb5239b79355a7fada467c865a04", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "true_interp", "typing_EverCrypt.AEAD.alg_of_vale_impl", "typing_EverCrypt.CTR.Keys.concrete_xkey_len", "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_FStar.UInt.fits", "typing_FStar.UInt32.add", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.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_unused_in", "typing_LowStar.Monotonic.Buffer.mgsub", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.is_supported_alg", "typing_Spec.Agile.AEAD.kv", "typing_Spec.Cipher.Expansion.cipher_alg_of_impl", "typing_Spec.Cipher.Expansion.concrete_xkey_length", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "9d36b8d3d81d698bbf58a10ad90cebbd" ], [ "EverCrypt.AEAD.alloca", 1, 0, 0, [ "@query" ], 0, "ccf2e68f19bdc36d529ac6cac413c537" ], [ "EverCrypt.AEAD.alloca", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "disc_equation_Spec.Agile.AEAD.AES128_GCM", "disc_equation_Spec.Agile.AEAD.AES256_GCM", "disc_equation_Spec.Agile.AEAD.CHACHA20_POLY1305", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equation_EverCrypt.AEAD.config_pre", "equation_Spec.Agile.AEAD.is_supported_alg", "refinement_interpretation_Tm_refine_0319fb5ba557ddfef833720396790fd1", "refinement_interpretation_Tm_refine_2eef4f5b3ef37e3ff95c04d51859e716", "refinement_interpretation_Tm_refine_99ada403f00103c1c9eb563019e967f7", "refinement_interpretation_Tm_refine_c85854d5f66a184b37bfa060ff70e13e", "refinement_interpretation_Tm_refine_e692cabf996d3cca074ab12757df58a8", "typing_Spec.Agile.AEAD.is_supported_alg" ], 0, "72bf81d0b771c3502db5cb6edbdc125b" ], [ "EverCrypt.AEAD.encrypt_gen_pre", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "e18f3137545523d3b806314573e9492a" ], [ "EverCrypt.AEAD.encrypt_pre", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_LowStar.Buffer.pointer_or_null", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.supported_alg", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc", "refinement_interpretation_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0", "typing_Spec.Agile.AEAD.is_supported_alg" ], 0, "0608fac85c347326e5146e399a5c0b3e" ], [ "EverCrypt.AEAD.encrypt_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.plain_p", "equation_EverCrypt.CTR.Keys.uint8", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer_or_null", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.GaloisField.gf", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_LowStar.Buffer.trivial_preorder", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "0419c4e3b2fa4bb92eabef9f5c5dee00" ], [ "EverCrypt.AEAD.aes_gcm_encrypt", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "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.Cipher.Expansion.Vale_AES128", "disc_equation_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equality_tok_Vale.AES.AES_s.AES_128@tok", "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_EverCrypt.CTR.Keys.vale_alg_of_vale_impl", "equation_EverCrypt.CTR.Keys.vale_impl", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_344ec675ebd831e2122dcf7c68ea1093", "refinement_interpretation_Tm_refine_35b13382ff5ad54d06f2db1bd5f09c8b", "refinement_interpretation_Tm_refine_a13c8f1281f5a23fd5f993c3af9de6a4", "refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_EverCrypt.CTR.Keys.vale_alg_of_vale_impl", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "unit_typing" ], 0, "3c6bc1e7181c66deb29a819521b0139f" ], [ "EverCrypt.AEAD.encrypt_aes_gcm", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "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.Signed", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S64", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.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.AES.AES128", "constructor_distinct_Spec.AES.AES256", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.Cipher.AES128", "constructor_distinct_Spec.Agile.Cipher.AES256", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "constructor_distinct_Tm_unit", "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.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.AES.AES128@tok", "equality_tok_Spec.AES.AES256@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.Cipher.AES128@tok", "equality_tok_Spec.Agile.Cipher.AES256@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@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.alg_of_vale_impl", "equation_EverCrypt.AEAD.as_kv", "equation_EverCrypt.AEAD.config_pre", "equation_EverCrypt.AEAD.encrypt_live_disjoint_pre", "equation_EverCrypt.AEAD.encrypt_pre", "equation_EverCrypt.AEAD.footprint", "equation_EverCrypt.AEAD.footprint_s", "equation_EverCrypt.AEAD.freeable", "equation_EverCrypt.AEAD.invariant", "equation_EverCrypt.AEAD.invariant_s", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.plain_p", "equation_EverCrypt.AEAD.preserves_freeable", "equation_EverCrypt.AEAD.state", "equation_EverCrypt.AEAD.supported_alg_of_impl", "equation_EverCrypt.CTR.Keys.concrete_xkey_len", "equation_EverCrypt.CTR.Keys.key_offset", "equation_EverCrypt.CTR.Keys.uint8", "equation_EverCrypt.CTR.Keys.vale_alg_of_vale_impl", "equation_EverCrypt.CTR.Keys.vale_impl", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Int.Cast.uint32_to_uint64", "equation_FStar.Integers.int_t", "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_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "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_LowStar.Monotonic.Buffer.loc_in", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.aes_key", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.AES.key_size", "equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg", "equation_Spec.Agile.AEAD.encrypt", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.iv_length", "equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.kv", "equation_Spec.Agile.AEAD.lbytes", "equation_Spec.Agile.AEAD.tag_length", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.AEAD.uu___2", "equation_Spec.Agile.AEAD.vale_alg_of_alg", "equation_Spec.Agile.Cipher.aes_alg_of_alg", "equation_Spec.Agile.Cipher.key", "equation_Spec.Agile.Cipher.key_length", "equation_Spec.Chacha20.size_key", "equation_Spec.Cipher.Expansion.cipher_alg_of_impl", "equation_Spec.Cipher.Expansion.concrete_expand", "equation_Spec.Cipher.Expansion.concrete_xkey", "equation_Spec.Cipher.Expansion.concrete_xkey_length", "equation_Spec.Cipher.Expansion.vale_aes_expansion", "equation_Spec.Cipher.Expansion.vale_alg_of_cipher_alg", "equation_Spec.Cipher.Expansion.vale_xkey_length", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "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.GCM_s.supported_iv_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_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", "fuel_guarded_inversion_Spec.Agile.AEAD.alg", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Spec.Agile.AEAD.uu___2", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "inversion-interp", "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_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.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_init_len", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "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.gsub_gsub", "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.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_idem", "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", "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_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_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.Mktuple2__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_1e64982fd73e0ea5a2ac3364e3b86e76", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_2cdcf23dde76eaaabed8d3b7a2d3160d", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_2de624c162d100733662a5fed8d478ed", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_709aff84c75b0fff77dcbf3b529649dd", "refinement_interpretation_Tm_refine_7862c213aa971a975331dc02dfe230e1", "refinement_interpretation_Tm_refine_79f1f8b4d6774015af27e4432311c913", "refinement_interpretation_Tm_refine_7c655d1405629ff643b03074f7df95c0", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8d45d8b47d49c79d2c9a76c0f9cd4104", "refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955", "refinement_interpretation_Tm_refine_9100ab96093283c751c14419f2de4403", "refinement_interpretation_Tm_refine_982fb3d3fec67274e50be352a80fb36e", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_b673b32f5af6ea360a97307ffc0b9719", "refinement_interpretation_Tm_refine_bdb8e2f4b5a690ae0ff20fed002844e2", "refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_dd592ff911d0f80cdf0ace6c4224ff73", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e86c95ce88afc69c180cbf98a0593f5d", "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_8f53c9bd715d5bf10798304ebe2c54e8", "true_interp", "typing_EverCrypt.AEAD.alg_of_vale_impl", "typing_EverCrypt.AEAD.footprint", "typing_EverCrypt.AEAD.footprint_s", "typing_EverCrypt.CTR.Keys.concrete_xkey_len", "typing_EverCrypt.CTR.Keys.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.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.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.UInt32.add", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.length", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.is_supported_alg", "typing_Spec.Agile.AEAD.tag_length", "typing_Spec.Cipher.Expansion.concrete_expand", "typing_Spec.Cipher.Expansion.concrete_xkey_length", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.AES.AES_s.aes_encrypt_LE", "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_to_seq_four_LE", "typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8", "typing_tok_EverCrypt.Error.InvalidKey@tok", "typing_tok_EverCrypt.Error.Success@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Vale.AES.AES_s.AES_128@tok", "typing_tok_Vale.AES.AES_s.AES_256@tok" ], 0, "d1d4157f8f87599f5c75108827f80f4c" ], [ "EverCrypt.AEAD.encrypt_aes128_gcm", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.Agile.AEAD.is_supported_alg", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3e9a939c523db9441d96f9f909e76ac9", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_53e8cc0cfd1bb9ba99c4a1e39547aec9", "refinement_interpretation_Tm_refine_9dce610ece0fab2fc6bf76bb9f61357e", "refinement_interpretation_Tm_refine_e922a86b7951c91519d5a12fc9fae388", "typing_EverCrypt.TargetConfig.x64" ], 0, "08c5c8b33aa8d0f1885cc4841be93e5d" ], [ "EverCrypt.AEAD.encrypt_aes256_gcm", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.Agile.AEAD.is_supported_alg", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_706054f4b8ee60ffa372f88088e425be", "refinement_interpretation_Tm_refine_bb420391019b08a67df8b6b95c3fc57c", "refinement_interpretation_Tm_refine_d86900c1d57c221a4faadb77a6a366e1", "refinement_interpretation_Tm_refine_f597dcffef4571f790e6ffb290657179", "typing_EverCrypt.TargetConfig.x64" ], 0, "ef70003a88d5c66d3b60951eb46428ae" ], [ "EverCrypt.AEAD.encrypt", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "e55841a281906e4df3c773ce6a756422" ], [ "EverCrypt.AEAD.encrypt", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_EverCrypt.Error.InvalidKey", "constructor_distinct_EverCrypt.Error.Success", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "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.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Cipher.Expansion.Hacl_CHACHA20", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "disc_equation_Spec.Cipher.Expansion.Hacl_CHACHA20", "disc_equation_Spec.Cipher.Expansion.Vale_AES128", "disc_equation_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_EverCrypt.Error.InvalidKey@tok", "equality_tok_EverCrypt.Error.Success@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Cipher.Expansion.Hacl_CHACHA20@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.as_kv", "equation_EverCrypt.AEAD.config_pre", "equation_EverCrypt.AEAD.encrypt_live_disjoint_pre", "equation_EverCrypt.AEAD.encrypt_pre", "equation_EverCrypt.AEAD.footprint", "equation_EverCrypt.AEAD.footprint_s", "equation_EverCrypt.AEAD.freeable", "equation_EverCrypt.AEAD.invariant", "equation_EverCrypt.AEAD.invariant_s", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.plain_p", "equation_EverCrypt.AEAD.preserves_freeable", "equation_EverCrypt.AEAD.state", "equation_EverCrypt.AEAD.supported_alg_of_impl", "equation_EverCrypt.CTR.Keys.uint8", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_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.int_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.unsigned", "equation_Lib.IntTypes.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", "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.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.ad", "equation_Spec.Agile.AEAD.cipher", "equation_Spec.Agile.AEAD.cipher_length", "equation_Spec.Agile.AEAD.encrypt", "equation_Spec.Agile.AEAD.encrypted", "equation_Spec.Agile.AEAD.iv", "equation_Spec.Agile.AEAD.iv_length", "equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.kv", "equation_Spec.Agile.AEAD.lbytes", "equation_Spec.Agile.AEAD.max_length", "equation_Spec.Agile.AEAD.plain", "equation_Spec.Agile.AEAD.supported_alg", "equation_Spec.Agile.AEAD.tag_length", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.Chacha20.size_key", "equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20Poly1305.aead_encrypt", "equation_Spec.Chacha20Poly1305.key", "equation_Spec.Chacha20Poly1305.nonce", "equation_Spec.Chacha20Poly1305.size_key", "equation_Spec.Chacha20Poly1305.size_nonce", "equation_Spec.Cipher.Expansion.concrete_expand", "equation_Spec.Cipher.Expansion.concrete_xkey_length", "equation_Spec.Cipher.Expansion.uu___30", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "fuel_guarded_inversion_Spec.Cipher.Expansion.impl", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "function_token_typing_Spec.Cipher.Expansion.uu___30", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing", "inversion-interp", "kinding_EverCrypt.AEAD.state_s@tok", "lemma_EverCrypt.AEAD.frame_invariant", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.Sequence.eq_elim", "lemma_LowStar.Monotonic.Buffer.as_seq_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_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.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality", "proj_equation_Spec.GaloisField.GF_t", "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_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_1cc41c3630856663dcfa11216c896f06", "refinement_interpretation_Tm_refine_1e64982fd73e0ea5a2ac3364e3b86e76", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_3e9a939c523db9441d96f9f909e76ac9", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_441053ce797e25d73d24fdb378a43afc", "refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_615cdbff9e4be4b2687efb17f829c7c1", "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0", "refinement_interpretation_Tm_refine_9315e6f2e6143f3996b9238ef3ae182b", "refinement_interpretation_Tm_refine_982fb3d3fec67274e50be352a80fb36e", "refinement_interpretation_Tm_refine_9c278566a1076c216e9de7ddec9e41a6", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_b19a1c83769dccbdda4cf44bd4e3d295", "refinement_interpretation_Tm_refine_bb420391019b08a67df8b6b95c3fc57c", "refinement_interpretation_Tm_refine_bdb8e2f4b5a690ae0ff20fed002844e2", "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc", "refinement_interpretation_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_dd6b7c82943901495ce61ec2042328d2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e6471c192f70c5d96f8a4a619c9552e7", "refinement_interpretation_Tm_refine_e86c95ce88afc69c180cbf98a0593f5d", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fb77d4109290540100357b20e0a78486", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0", "typing_EverCrypt.AEAD.footprint_s", "typing_FStar.Ghost.reveal", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar", "typing_Lib.IntTypes.unsigned", "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_LowStar.Monotonic.Buffer.mgsub", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.encrypt", "typing_Spec.Agile.AEAD.kv", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_EverCrypt.Error.InvalidKey@tok", "typing_tok_EverCrypt.Error.Success@tok", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "9720f9f0c86d1b0183e0d15310ef2976" ], [ "EverCrypt.AEAD.encrypt_expand_pre", 1, 0, 0, [ "@query" ], 0, "ad291ae1beab259094aa69de807c7833" ], [ "EverCrypt.AEAD.encrypt_expand_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.plain_p", "equation_EverCrypt.CTR.Keys.uint8", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Agile.AEAD.uint8", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_e692cabf996d3cca074ab12757df58a8", "typing_LowStar.Buffer.trivial_preorder" ], 0, "e069a222a761d015ce806ebe40baf2ee" ], [ "EverCrypt.AEAD.encrypt_expand_aes_gcm", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "constructor_distinct_EverCrypt.Error.Success", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_EverCrypt.Error.Success@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_EverCrypt.AEAD.encrypt_expand_pre", "equation_EverCrypt.AEAD.encrypt_gen_pre", "equation_EverCrypt.AEAD.encrypt_live_disjoint_pre", "equation_EverCrypt.AEAD.encrypt_pre", "equation_EverCrypt.AEAD.footprint", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.plain_p", "equation_EverCrypt.AEAD.state", "equation_EverCrypt.CTR.Keys.uint8", "equation_EverCrypt.CTR.Keys.vale_impl", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "kinding_EverCrypt.AEAD.state_s@tok", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_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_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "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.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_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_1e64982fd73e0ea5a2ac3364e3b86e76", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4bd749d770b312dee1e14ff3de520d9c", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_7c655d1405629ff643b03074f7df95c0", "refinement_interpretation_Tm_refine_8d45d8b47d49c79d2c9a76c0f9cd4104", "refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35", "refinement_interpretation_Tm_refine_c4fea1cb1fba11da5838397b5ec2f3e9", "refinement_interpretation_Tm_refine_cc39cb5239b79355a7fada467c865a04", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.AEAD.alg_of_vale_impl", "typing_EverCrypt.AEAD.footprint", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_EverCrypt.Error.Success@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "235c661e728ec6c04abb46a97a7751d0" ], [ "EverCrypt.AEAD.encrypt_expand_aes128_gcm_no_check", 1, 0, 0, [ "@query", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equation_Spec.Agile.AEAD.is_supported_alg", "projection_inverse_BoxBool_proj_0" ], 0, "c43781f2159491f634f2ab68af01c987" ], [ "EverCrypt.AEAD.encrypt_expand_aes128_gcm_no_check", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_EverCrypt.Error.Success", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "equality_tok_EverCrypt.Error.Success@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4c60e089d318ef86f026b776c98732f2", "refinement_interpretation_Tm_refine_53e8cc0cfd1bb9ba99c4a1e39547aec9", "refinement_interpretation_Tm_refine_65382ef07b34f619ca3dd785b2bcf1de", "refinement_interpretation_Tm_refine_d6f59a691590d80420f67dcedef36cc8", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e922a86b7951c91519d5a12fc9fae388", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_EverCrypt.Error.Success@tok" ], 0, "dda1a46abc05df80478f77540b556939" ], [ "EverCrypt.AEAD.encrypt_expand_aes256_gcm_no_check", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "4dd4d33cfc7d69556177303cae86f7dc" ], [ "EverCrypt.AEAD.encrypt_expand_aes256_gcm_no_check", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_EverCrypt.Error.Success", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_EverCrypt.Error.Success@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_02e5df6b3b9437346ab811e066aeac60", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_706054f4b8ee60ffa372f88088e425be", "refinement_interpretation_Tm_refine_a27d87900f03b1f7f052fd6f120cb378", "refinement_interpretation_Tm_refine_b32ee0eeb5a644a1ba94f9e61404d8c7", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f597dcffef4571f790e6ffb290657179", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_EverCrypt.Error.Success@tok" ], 0, "a00e1ed180b20f28692c80252f06fc53" ], [ "EverCrypt.AEAD.encrypt_expand_aes128_gcm", 1, 0, 0, [ "@query", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equation_Spec.Agile.AEAD.is_supported_alg", "projection_inverse_BoxBool_proj_0" ], 0, "e9e3e5435fa3a08052e981df9c28411b" ], [ "EverCrypt.AEAD.encrypt_expand_aes128_gcm", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_EverCrypt.Error.Success", "constructor_distinct_EverCrypt.Error.UnsupportedAlgorithm", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "equality_tok_EverCrypt.Error.Success@tok", "equality_tok_EverCrypt.Error.UnsupportedAlgorithm@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_EverCrypt.AEAD.config_pre", "equation_EverCrypt.AEAD.encrypt_expand_pre", "equation_EverCrypt.AEAD.encrypt_gen_pre", "equation_EverCrypt.AEAD.encrypt_live_disjoint_pre", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.plain_p", "equation_EverCrypt.CTR.Keys.uint8", "equation_FStar.Monotonic.HyperStack.live_region", "equation_FStar.Monotonic.HyperStack.mem", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "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_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_AmpAmp", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_1e64982fd73e0ea5a2ac3364e3b86e76", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_271aba192dc650e86535ca510fdec348", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_53e8cc0cfd1bb9ba99c4a1e39547aec9", "refinement_interpretation_Tm_refine_65382ef07b34f619ca3dd785b2bcf1de", "refinement_interpretation_Tm_refine_bdb8e2f4b5a690ae0ff20fed002844e2", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_d6f59a691590d80420f67dcedef36cc8", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e86c95ce88afc69c180cbf98a0593f5d", "refinement_interpretation_Tm_refine_e922a86b7951c91519d5a12fc9fae388", "typing_FStar.Monotonic.HyperStack.live_region", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_EverCrypt.Error.Success@tok", "typing_tok_EverCrypt.Error.UnsupportedAlgorithm@tok" ], 0, "308182f59f1283623c258062e261cd0b" ], [ "EverCrypt.AEAD.encrypt_expand_aes256_gcm", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "1c7474518b53106a40a68c135ff2ab1b" ], [ "EverCrypt.AEAD.encrypt_expand_aes256_gcm", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_EverCrypt.Error.Success", "constructor_distinct_EverCrypt.Error.UnsupportedAlgorithm", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_EverCrypt.Error.Success@tok", "equality_tok_EverCrypt.Error.UnsupportedAlgorithm@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_EverCrypt.AEAD.config_pre", "equation_EverCrypt.AEAD.encrypt_expand_pre", "equation_EverCrypt.AEAD.encrypt_gen_pre", "equation_EverCrypt.AEAD.encrypt_live_disjoint_pre", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.plain_p", "equation_EverCrypt.CTR.Keys.uint8", "equation_FStar.Monotonic.HyperStack.mem", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_AmpAmp", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_02e5df6b3b9437346ab811e066aeac60", "refinement_interpretation_Tm_refine_1e64982fd73e0ea5a2ac3364e3b86e76", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_6cf8498a5bc737c23300b62503046fd1", "refinement_interpretation_Tm_refine_706054f4b8ee60ffa372f88088e425be", "refinement_interpretation_Tm_refine_b32ee0eeb5a644a1ba94f9e61404d8c7", "refinement_interpretation_Tm_refine_bdb8e2f4b5a690ae0ff20fed002844e2", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e86c95ce88afc69c180cbf98a0593f5d", "refinement_interpretation_Tm_refine_f597dcffef4571f790e6ffb290657179", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_EverCrypt.Error.Success@tok", "typing_tok_EverCrypt.Error.UnsupportedAlgorithm@tok" ], 0, "103d81306cb700e3215c6408a5111094" ], [ "EverCrypt.AEAD.encrypt_expand_chacha20_poly1305", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "0440d12c3bc4d30d7ce5a101c4dcb592" ], [ "EverCrypt.AEAD.encrypt_expand_chacha20_poly1305", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_EverCrypt.Error.Success", "constructor_distinct_FStar.Integers.Signed", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.Cipher.CHACHA20", "equality_tok_EverCrypt.Error.Success@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.Cipher.CHACHA20@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.as_kv", "equation_EverCrypt.AEAD.encrypt_expand_pre", "equation_EverCrypt.AEAD.encrypt_gen_pre", "equation_EverCrypt.AEAD.encrypt_live_disjoint_pre", "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_EverCrypt.AEAD.supported_alg_of_impl", "equation_EverCrypt.CTR.Keys.uint8", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Integers.int_t", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_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.int_t", "equation_Lib.IntTypes.minint", "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.unsigned", "equation_Lib.IntTypes.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", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.ad", "equation_Spec.Agile.AEAD.cipher", "equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg", "equation_Spec.Agile.AEAD.encrypt", "equation_Spec.Agile.AEAD.encrypted", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.iv", "equation_Spec.Agile.AEAD.iv_length", "equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.max_length", "equation_Spec.Agile.AEAD.plain", "equation_Spec.Agile.AEAD.tag_length", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.Cipher.key_length", "equation_Spec.Chacha20.chacha20_encrypt_bytes", "equation_Spec.Chacha20.counter", "equation_Spec.Chacha20.key", "equation_Spec.Chacha20.nonce", "equation_Spec.Chacha20.size_block", "equation_Spec.Chacha20.size_key", "equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20Poly1305.aead_encrypt", "equation_Spec.Chacha20Poly1305.key", "equation_Spec.Chacha20Poly1305.nonce", "equation_Spec.Chacha20Poly1305.poly1305_do", "equation_Spec.Chacha20Poly1305.size_key", "equation_Spec.Chacha20Poly1305.size_nonce", "equation_Spec.Cipher.Expansion.concrete_expand", "equation_Spec.Cipher.Expansion.concrete_xkey_length", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.poly1305_finish", "equation_Spec.Poly1305.size_block", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "kinding_EverCrypt.AEAD.state_s@tok", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.Seq.Base.lemma_len_append", "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.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.Sequence.eq_elim", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_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_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_remove_new_locs", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_EverCrypt.AEAD.Ek_ek", "projection_inverse_EverCrypt.AEAD.Ek_impl", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0319fb5ba557ddfef833720396790fd1", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_1cc41c3630856663dcfa11216c896f06", "refinement_interpretation_Tm_refine_1e64982fd73e0ea5a2ac3364e3b86e76", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_28c7ab7e2e3881c52f6b844840d99221", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_3adad2fa15bf57cd1bb4986f7f40a94b", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_615cdbff9e4be4b2687efb17f829c7c1", "refinement_interpretation_Tm_refine_6ea782d20d3a5b4d53411900c5408b2a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7f16c7b57ef8bef37e694fdc293f58a5", "refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0", "refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955", "refinement_interpretation_Tm_refine_9315e6f2e6143f3996b9238ef3ae182b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_b19a1c83769dccbdda4cf44bd4e3d295", "refinement_interpretation_Tm_refine_bb80dc53cd8ef895a0bc33609981d9b5", "refinement_interpretation_Tm_refine_bc5dd0f8b2720074d1874478666f1f6b", "refinement_interpretation_Tm_refine_bdb8e2f4b5a690ae0ff20fed002844e2", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_dd6b7c82943901495ce61ec2042328d2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_de974ede28db942f3b8917b0054bb701", "refinement_interpretation_Tm_refine_e86c95ce88afc69c180cbf98a0593f5d", "refinement_interpretation_Tm_refine_e9f6b72af00281e5fb85d6d617f4ae4e", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f1f3a6a6d3da045b35e7ba130c8b362a", "refinement_interpretation_Tm_refine_fb77d4109290540100357b20e0a78486", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.AEAD.as_kv", "typing_EverCrypt.AEAD.footprint_s", "typing_EverCrypt.AEAD.supported_alg_of_impl", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length", "typing_FStar.Set.complement", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar", "typing_Lib.ByteSequence.nat_to_bytes_le", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.unsigned", "typing_Lib.Sequence.concat", "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_LowStar.Monotonic.Buffer.mgsub", "typing_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.encrypt", "typing_Spec.Agile.AEAD.tag_length", "typing_Spec.Chacha20.chacha20_encrypt_bytes", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_tok_EverCrypt.Error.Success@tok", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok" ], 0, "dbc1dc8259f87a43966d6b853622e721" ], [ "EverCrypt.AEAD.encrypt_expand", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "f1a36cb97716a9d825a6124f71551cdc" ], [ "EverCrypt.AEAD.encrypt_expand", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_EverCrypt.Error.Success", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "disc_equation_Spec.Agile.AEAD.AES128_GCM", "disc_equation_Spec.Agile.AEAD.AES256_GCM", "disc_equation_Spec.Agile.AEAD.CHACHA20_POLY1305", "equality_tok_EverCrypt.Error.Success@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.config_pre", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.plain_p", "equation_Spec.Agile.AEAD.iv_length", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_271aba192dc650e86535ca510fdec348", "refinement_interpretation_Tm_refine_4a2fab199af0b7c10817924a17a0d1b6", "refinement_interpretation_Tm_refine_5cbf4890acb5de88617d741c6e62c29d", "refinement_interpretation_Tm_refine_6cf8498a5bc737c23300b62503046fd1", "refinement_interpretation_Tm_refine_bc5dd0f8b2720074d1874478666f1f6b", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_d573e930eb40dc14f3bec28511a6b760", "refinement_interpretation_Tm_refine_e692cabf996d3cca074ab12757df58a8", "typing_tok_EverCrypt.Error.Success@tok" ], 0, "c28d5eac4c48a446ee958bcc67ab7fed" ], [ "EverCrypt.AEAD.decrypt_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.cipher_p", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.CTR.Keys.uint8", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer_or_null", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.max_length", "equation_Spec.Agile.AEAD.supported_alg", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.GaloisField.gf", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_Addition", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4a2fab199af0b7c10817924a17a0d1b6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955", "refinement_interpretation_Tm_refine_9e5d748a0876a43b3055c6e74cacea51", "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc", "refinement_interpretation_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.length", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.tag_length", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "566fb335e8f200506eb84d41418a372d" ], [ "EverCrypt.AEAD.aes_gcm_decrypt", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "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.Cipher.Expansion.Vale_AES128", "disc_equation_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equality_tok_Vale.AES.AES_s.AES_128@tok", "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_EverCrypt.CTR.Keys.vale_alg_of_vale_impl", "equation_EverCrypt.CTR.Keys.vale_impl", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_1d900e57fd475dca8c311469282759de", "refinement_interpretation_Tm_refine_308913f3d99e5d8dd2a9f4364f3735a9", "refinement_interpretation_Tm_refine_37dbc9e173f9e617022815b7334b6969", "refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_EverCrypt.CTR.Keys.vale_alg_of_vale_impl", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "unit_typing" ], 0, "262c9c4f65788dfe26c06074d05263a1" ], [ "EverCrypt.AEAD.decrypt_aes_gcm", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "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.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_FStar.Pervasives.Native.None", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S64", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.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.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.AES.AES128", "constructor_distinct_Spec.AES.AES256", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.Cipher.AES128", "constructor_distinct_Spec.Agile.Cipher.AES256", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "constructor_distinct_Tm_unit", "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.W32@tok", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.AES.AES128@tok", "equality_tok_Spec.AES.AES256@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.Cipher.AES128@tok", "equality_tok_Spec.Agile.Cipher.AES256@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@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.alg_of_vale_impl", "equation_EverCrypt.AEAD.as_kv", "equation_EverCrypt.AEAD.cipher_p", "equation_EverCrypt.AEAD.config_pre", "equation_EverCrypt.AEAD.footprint", "equation_EverCrypt.AEAD.footprint_s", "equation_EverCrypt.AEAD.freeable", "equation_EverCrypt.AEAD.invariant", "equation_EverCrypt.AEAD.invariant_s", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.preserves_freeable", "equation_EverCrypt.AEAD.state", "equation_EverCrypt.AEAD.supported_alg_of_impl", "equation_EverCrypt.CTR.Keys.concrete_xkey_len", "equation_EverCrypt.CTR.Keys.key_offset", "equation_EverCrypt.CTR.Keys.uint8", "equation_EverCrypt.CTR.Keys.vale_alg_of_vale_impl", "equation_EverCrypt.CTR.Keys.vale_impl", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Int.Cast.uint32_to_uint64", "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_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "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_LowStar.Monotonic.Buffer.loc_in", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.aes_key", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.AES.key_size", "equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg", "equation_Spec.Agile.AEAD.decrypt", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.iv_length", "equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.kv", "equation_Spec.Agile.AEAD.lbytes", "equation_Spec.Agile.AEAD.tag_length", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.AEAD.uu___2", "equation_Spec.Agile.AEAD.vale_alg_of_alg", "equation_Spec.Agile.Cipher.aes_alg_of_alg", "equation_Spec.Agile.Cipher.key", "equation_Spec.Agile.Cipher.key_length", "equation_Spec.Chacha20.size_key", "equation_Spec.Cipher.Expansion.cipher_alg_of_impl", "equation_Spec.Cipher.Expansion.concrete_expand", "equation_Spec.Cipher.Expansion.concrete_xkey", "equation_Spec.Cipher.Expansion.concrete_xkey_length", "equation_Spec.Cipher.Expansion.vale_aes_expansion", "equation_Spec.Cipher.Expansion.vale_alg_of_cipher_alg", "equation_Spec.Cipher.Expansion.vale_xkey_length", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "equation_Vale.AES.AES_s.is_aes_key", "equation_Vale.AES.AES_s.is_aes_key_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_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_Spec.Agile.AEAD.alg", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "function_token_typing_Spec.Agile.AEAD.uu___2", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "inversion-interp", "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_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.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_init_len", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_FStar.UInt64.uv_inv", "lemma_FStar.UInt64.vu_inv", "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.gsub_gsub", "lemma_LowStar.Monotonic.Buffer.len_gsub", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "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_idem", "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", "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_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Spec.GaloisField.GF_t", "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", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_1e64982fd73e0ea5a2ac3364e3b86e76", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_2cdcf23dde76eaaabed8d3b7a2d3160d", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_2de624c162d100733662a5fed8d478ed", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_4a9f5a632ccb67c4adcfd65a1dab0c7c", "refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019", "refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_66d93998af0c5b273a2b1ea81a0c3bb1", "refinement_interpretation_Tm_refine_709aff84c75b0fff77dcbf3b529649dd", "refinement_interpretation_Tm_refine_79f1f8b4d6774015af27e4432311c913", "refinement_interpretation_Tm_refine_7c655d1405629ff643b03074f7df95c0", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_8f75026f76b9bbf3ca23349b2eb67751", "refinement_interpretation_Tm_refine_9100ab96093283c751c14419f2de4403", "refinement_interpretation_Tm_refine_982fb3d3fec67274e50be352a80fb36e", "refinement_interpretation_Tm_refine_9e5d748a0876a43b3055c6e74cacea51", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_bdb8e2f4b5a690ae0ff20fed002844e2", "refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_d15a9766d4c1ec94d1574f05b54a618b", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_dd592ff911d0f80cdf0ace6c4224ff73", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e86c95ce88afc69c180cbf98a0593f5d", "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f62981b95c40f715ab60acc51220aa6c", "refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "true_interp", "typing_EverCrypt.AEAD.alg_of_vale_impl", "typing_EverCrypt.AEAD.footprint", "typing_EverCrypt.AEAD.footprint_s", "typing_EverCrypt.CTR.Keys.concrete_xkey_len", "typing_EverCrypt.CTR.Keys.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.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Monotonic.HyperStack.mk_mem", "typing_FStar.Monotonic.HyperStack.pop", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt.fits", "typing_FStar.UInt32.add", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.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_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_LowStar.Monotonic.Buffer.mgsub", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.is_supported_alg", "typing_Spec.Cipher.Expansion.concrete_expand", "typing_Spec.Cipher.Expansion.concrete_xkey_length", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.AES.AES_s.aes_encrypt_LE", "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_to_seq_four_LE", "typing_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8", "typing_tok_EverCrypt.Error.AuthenticationFailure@tok", "typing_tok_EverCrypt.Error.InvalidKey@tok", "typing_tok_EverCrypt.Error.Success@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Vale.AES.AES_s.AES_256@tok" ], 0, "d9e105fb9f2e74c3be6c1bb2b101c906" ], [ "EverCrypt.AEAD.decrypt_aes128_gcm", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.Agile.AEAD.is_supported_alg", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_273338279bf37cbeeea1300ffa8034be", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_51c368638c898154286989c300105539", "refinement_interpretation_Tm_refine_e922a86b7951c91519d5a12fc9fae388", "typing_EverCrypt.TargetConfig.x64" ], 0, "5061214e6194fc2d4307c4c826902a79" ], [ "EverCrypt.AEAD.decrypt_aes256_gcm", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.Agile.AEAD.is_supported_alg", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_295569119c81646492ddb7b407c3c519", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_490c36c4fc777a7f67d3759a31e7e8c0", "refinement_interpretation_Tm_refine_f597dcffef4571f790e6ffb290657179", "typing_EverCrypt.TargetConfig.x64" ], 0, "19f7a5d3f24e5d2e3211dc360c3445e2" ], [ "EverCrypt.AEAD.decrypt_chacha20_poly1305", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "083ef5c3baa92eadfe6aafee415e1f39" ], [ "EverCrypt.AEAD.decrypt_chacha20_poly1305", 2, 0, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "LowStar.Monotonic.Buffer_interpretation_Tm_ghost_arrow_6f11043f8e60f5b9238b8b3413d1922c", "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.W16", "constructor_distinct_FStar.Integers.W32", "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.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.Cipher.CHACHA20", "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.W32@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.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.Cipher.CHACHA20@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.as_kv", "equation_EverCrypt.AEAD.cipher_p", "equation_EverCrypt.AEAD.footprint", "equation_EverCrypt.AEAD.footprint_s", "equation_EverCrypt.AEAD.freeable", "equation_EverCrypt.AEAD.invariant", "equation_EverCrypt.AEAD.invariant_s", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.preserves_freeable", "equation_EverCrypt.AEAD.state", "equation_EverCrypt.AEAD.supported_alg_of_impl", "equation_EverCrypt.CTR.Keys.uint8", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_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.int_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.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "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.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg", "equation_Spec.Agile.AEAD.decrypt", "equation_Spec.Agile.AEAD.decrypted", "equation_Spec.Agile.AEAD.iv_length", "equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.kv", "equation_Spec.Agile.AEAD.lbytes", "equation_Spec.Agile.AEAD.max_length", "equation_Spec.Agile.AEAD.tag_length", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.Cipher.key_length", "equation_Spec.Chacha20.size_key", "equation_Spec.Chacha20Poly1305.aead_decrypt", "equation_Spec.Cipher.Expansion.concrete_expand", "equation_Spec.Cipher.Expansion.concrete_xkey_length", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Monotonic.Buffer.loc_union", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "kinding_EverCrypt.AEAD.state_s@tok", "lemma_EverCrypt.AEAD.frame_invariant", "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.Seq.Properties.slice_length", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "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.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "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", "primitive_Prims.op_disEquality", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Spec.GaloisField.GF_t", "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.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_1e64982fd73e0ea5a2ac3364e3b86e76", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_28c7ab7e2e3881c52f6b844840d99221", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_66d93998af0c5b273a2b1ea81a0c3bb1", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_89d4ad03bf0ef5b8cab53755ffc32429", "refinement_interpretation_Tm_refine_982fb3d3fec67274e50be352a80fb36e", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_9e5d748a0876a43b3055c6e74cacea51", "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b", "refinement_interpretation_Tm_refine_bdb8e2f4b5a690ae0ff20fed002844e2", "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e86c95ce88afc69c180cbf98a0593f5d", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fa0e7eeef3636052a107ed15123aceaf", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.AEAD.footprint", "typing_EverCrypt.AEAD.footprint_s", "typing_FStar.Ghost.reveal", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.unsigned", "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_LowStar.Monotonic.Buffer.mgsub", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.kv", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_tok_EverCrypt.Error.AuthenticationFailure@tok", "typing_tok_EverCrypt.Error.InvalidKey@tok", "typing_tok_EverCrypt.Error.Success@tok", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok" ], 0, "88646ccfd5b614cb76e0f857cc7923ec" ], [ "EverCrypt.AEAD.decrypt_chacha20_poly1305", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "724de833d7c942efef16f2735406370d" ], [ "EverCrypt.AEAD.decrypt", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "aaf4dbebf690ef098c67996a85bbf54f" ], [ "EverCrypt.AEAD.decrypt", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_EverCrypt.Error.InvalidKey", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Cipher.Expansion.Hacl_CHACHA20", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "disc_equation_Spec.Cipher.Expansion.Hacl_CHACHA20", "disc_equation_Spec.Cipher.Expansion.Vale_AES128", "disc_equation_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_EverCrypt.Error.InvalidKey@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Hacl_CHACHA20@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.cipher_p", "equation_EverCrypt.AEAD.config_pre", "equation_EverCrypt.AEAD.invariant", "equation_EverCrypt.AEAD.invariant_s", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.supported_alg_of_impl", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer_or_null", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.supported_alg", "equation_Spec.Cipher.Expansion.uu___30", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Cipher.Expansion.impl", "function_token_typing_Spec.Cipher.Expansion.uu___30", "inversion-interp", "kinding_EverCrypt.AEAD.state_s@tok", "lemma_LowStar.Monotonic.Buffer.live_is_null", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_EverCrypt.AEAD.Ek_impl", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_273338279bf37cbeeea1300ffa8034be", "refinement_interpretation_Tm_refine_295569119c81646492ddb7b407c3c519", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_89d4ad03bf0ef5b8cab53755ffc32429", "refinement_interpretation_Tm_refine_9c278566a1076c216e9de7ddec9e41a6", "refinement_interpretation_Tm_refine_9e5d748a0876a43b3055c6e74cacea51", "refinement_interpretation_Tm_refine_ae73b51347bf47c4befe53573dedc34b", "refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc", "refinement_interpretation_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0", "typing_FStar.Ghost.reveal", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.g_is_null", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_EverCrypt.Error.InvalidKey@tok" ], 0, "fd2c3f86055910add80689780da0f828" ], [ "EverCrypt.AEAD.decrypt_expand_st", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.cipher_p", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.CTR.Keys.uint8", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Agile.AEAD.max_length", "equation_Spec.Agile.AEAD.uint8", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4a2fab199af0b7c10817924a17a0d1b6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9e5d748a0876a43b3055c6e74cacea51", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_e692cabf996d3cca074ab12757df58a8", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.length" ], 0, "50c0e8ffa44e914100d10e11f2900af2" ], [ "EverCrypt.AEAD.decrypt_expand_aes_gcm", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_EverCrypt.AEAD.cipher_p", "equation_EverCrypt.AEAD.footprint", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.state", "equation_EverCrypt.CTR.Keys.uint8", "equation_EverCrypt.CTR.Keys.vale_impl", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "kinding_EverCrypt.AEAD.state_s@tok", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Map.lemma_equal_elim", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "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_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_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.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_1e64982fd73e0ea5a2ac3364e3b86e76", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_56ca1e0454ec5c2925b2dd5f8c958f7a", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_7c655d1405629ff643b03074f7df95c0", "refinement_interpretation_Tm_refine_8f75026f76b9bbf3ca23349b2eb67751", "refinement_interpretation_Tm_refine_9e5d748a0876a43b3055c6e74cacea51", "refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35", "refinement_interpretation_Tm_refine_c4fea1cb1fba11da5838397b5ec2f3e9", "refinement_interpretation_Tm_refine_cc39cb5239b79355a7fada467c865a04", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.AEAD.alg_of_vale_impl", "typing_EverCrypt.AEAD.footprint", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "3c518f7c5dee4f28ad0938d292fb89af" ], [ "EverCrypt.AEAD.decrypt_expand_aes128_gcm_no_check", 1, 0, 0, [ "@query", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equation_Spec.Agile.AEAD.is_supported_alg", "projection_inverse_BoxBool_proj_0" ], 0, "d12dd5ca7c2d0972917e88b444afd5a1" ], [ "EverCrypt.AEAD.decrypt_expand_aes128_gcm_no_check", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_b41e18a01e168d42166793480c55da46", "refinement_interpretation_Tm_refine_d6f59a691590d80420f67dcedef36cc8", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e922a86b7951c91519d5a12fc9fae388", "refinement_interpretation_Tm_refine_f193c73ae4ca4f78f98990d48e71a65c", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "127717ca3ebaf412710ac4d19b55a63d" ], [ "EverCrypt.AEAD.decrypt_expand_aes256_gcm_no_check", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "f4cbbaed282fd4f3f47a5a839f86d57d" ], [ "EverCrypt.AEAD.decrypt_expand_aes256_gcm_no_check", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_95dfb38318c87a9ff23839b8cb3e024c", "refinement_interpretation_Tm_refine_b32ee0eeb5a644a1ba94f9e61404d8c7", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e3ce6fcffc5319c1c3da09a0c2710d29", "refinement_interpretation_Tm_refine_f597dcffef4571f790e6ffb290657179", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "6520a1b3872b63c61dedf3b93845270c" ], [ "EverCrypt.AEAD.decrypt_expand_aes128_gcm", 1, 0, 0, [ "@query", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equation_Spec.Agile.AEAD.is_supported_alg", "projection_inverse_BoxBool_proj_0" ], 0, "bbe28412c9835f0c281c6a468e636f72" ], [ "EverCrypt.AEAD.decrypt_expand_aes128_gcm", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_EverCrypt.Error.UnsupportedAlgorithm", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_EverCrypt.Error.UnsupportedAlgorithm@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_EverCrypt.AEAD.cipher_p", "equation_EverCrypt.AEAD.config_pre", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.CTR.Keys.uint8", "equation_FStar.Monotonic.HyperStack.live_region", "equation_FStar.Monotonic.HyperStack.mem", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "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_none", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_AmpAmp", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_1e64982fd73e0ea5a2ac3364e3b86e76", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_544f43b1b4ea48c13e3d3578d839de5a", "refinement_interpretation_Tm_refine_9e5d748a0876a43b3055c6e74cacea51", "refinement_interpretation_Tm_refine_b41e18a01e168d42166793480c55da46", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_d6f59a691590d80420f67dcedef36cc8", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e922a86b7951c91519d5a12fc9fae388", "typing_FStar.Monotonic.HyperStack.live_region", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_EverCrypt.Error.UnsupportedAlgorithm@tok" ], 0, "f4a6b9623b8de4a7b3851c3d028507b7" ], [ "EverCrypt.AEAD.decrypt_expand_aes256_gcm", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "2584762df5a8b0781d0b240a1e852b7e" ], [ "EverCrypt.AEAD.decrypt_expand_aes256_gcm", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_EverCrypt.Error.UnsupportedAlgorithm", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_EverCrypt.Error.UnsupportedAlgorithm@tok", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.alg_of_vale_impl", "equation_EverCrypt.AEAD.cipher_p", "equation_EverCrypt.AEAD.config_pre", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.CTR.Keys.uint8", "equation_FStar.Monotonic.HyperStack.mem", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_AmpAmp", "proj_equation_FStar.Pervasives.Native.Some_v", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_1e64982fd73e0ea5a2ac3364e3b86e76", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_544f43b1b4ea48c13e3d3578d839de5a", "refinement_interpretation_Tm_refine_9e5d748a0876a43b3055c6e74cacea51", "refinement_interpretation_Tm_refine_b32ee0eeb5a644a1ba94f9e61404d8c7", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e3ce6fcffc5319c1c3da09a0c2710d29", "refinement_interpretation_Tm_refine_f597dcffef4571f790e6ffb290657179", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_EverCrypt.Error.UnsupportedAlgorithm@tok" ], 0, "9e73a8b0b070f72c7a52b188d4756722" ], [ "EverCrypt.AEAD.decrypt_expand_chacha20_poly1305", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "5e3e3510ecac0ba7f8f94c3d5df3f86f" ], [ "EverCrypt.AEAD.decrypt_expand_chacha20_poly1305", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.cipher_p", "equation_EverCrypt.AEAD.footprint", "equation_EverCrypt.AEAD.iv_p", "equation_EverCrypt.AEAD.state", "equation_EverCrypt.CTR.Keys.uint8", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "kinding_EverCrypt.AEAD.state_s@tok", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Map.lemma_equal_elim", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "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_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_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.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0319fb5ba557ddfef833720396790fd1", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_1e64982fd73e0ea5a2ac3364e3b86e76", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_28c7ab7e2e3881c52f6b844840d99221", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_3adad2fa15bf57cd1bb4986f7f40a94b", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_7d628c9afa4eedea0cf75e43ce2844c1", "refinement_interpretation_Tm_refine_89d4ad03bf0ef5b8cab53755ffc32429", "refinement_interpretation_Tm_refine_9e5d748a0876a43b3055c6e74cacea51", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.AEAD.footprint", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.is_supported_alg", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok" ], 0, "61e945cc814e13a58f63d50adef6d75c" ], [ "EverCrypt.AEAD.decrypt_expand", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "5778aa13210508b4fcd3bb2f34ed0538" ], [ "EverCrypt.AEAD.decrypt_expand", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "disc_equation_Spec.Agile.AEAD.AES128_GCM", "disc_equation_Spec.Agile.AEAD.AES256_GCM", "disc_equation_Spec.Agile.AEAD.CHACHA20_POLY1305", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.cipher_p", "equation_EverCrypt.AEAD.config_pre", "equation_EverCrypt.AEAD.iv_p", "equation_Spec.Agile.AEAD.iv_length", "equation_Spec.Agile.AEAD.supported_alg", "lemma_FStar.Ghost.reveal_hide", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_1e5991971a05abb3200f8781b7e6ced0", "refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6", "refinement_interpretation_Tm_refine_544f43b1b4ea48c13e3d3578d839de5a", "refinement_interpretation_Tm_refine_6c8296a95dd15cc6fa3dabad38eb5405", "refinement_interpretation_Tm_refine_7d628c9afa4eedea0cf75e43ce2844c1", "refinement_interpretation_Tm_refine_9e5d748a0876a43b3055c6e74cacea51", "refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa", "refinement_kinding_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0" ], 0, "ebba58f8128668166ae4a375d84b1503" ], [ "EverCrypt.AEAD.free", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_typing", "constructor_distinct_FStar.Integers.Unsigned", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "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.Integers.int_t", "equation_FStar.Integers.uint_8", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.mem", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.supported_alg", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Integers.uint_8", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "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", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_EverCrypt.AEAD.Ek_ek", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_6e8915e7c4b3b516dfc7b6df43d91338", "refinement_interpretation_Tm_refine_bfb05b9ad724bdf137241c45fd0e2636", "refinement_interpretation_Tm_refine_c05f4f53dc4fe83beba2c2df56ce03ec", "refinement_interpretation_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_kinding_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0", "typing_EverCrypt.AEAD.footprint", "typing_EverCrypt.AEAD.footprint_s", "typing_FStar.Ghost.reveal", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Set.singleton", "typing_Lib.IntTypes.unsigned", "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", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "19f36e6796f56d465204cf233e31ad22" ] ] ]