Revision e56414221fb67ecff7d071497f8ba5d20e9c5ba9 authored by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC, committed by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC
1 parent db297bf
EverCrypt.AEAD.fst.hints
[
"�V�s�N)\u0011i���",
[
[
"EverCrypt.AEAD.uu___0",
1,
0,
0,
[ "@query" ],
0,
"d092aa6d0be829dc74bc8f9134619584"
],
[
"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,
"0430b8bf17114475c3ed915e48fdb5f6"
],
[
"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,
"2b54193b7d4cb03c9853250b838e0147"
],
[
"EverCrypt.AEAD.loc_includes_union_l_footprint_s",
1,
0,
0,
[ "@query" ],
0,
"e1a1e40b3fbd98a1a2064cd8ac87695a"
],
[
"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.W128",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.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",
"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.W128@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.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",
"equation_EverCrypt.AEAD.supported_alg_of_impl",
"equation_FStar.Pervasives.inversion", "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_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.GaloisField.gf", "equation_Spec.Poly1305.size_block",
"fuel_guarded_inversion_Spec.Cipher.Expansion.impl",
"function_token_typing_Prims.int",
"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_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_982fb3d3fec67274e50be352a80fb36e",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"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,
"acd52d92c30cb5db94300c2ec46efd58"
],
[
"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,
"aa32646191dcbdbc7ca470ffd31f3ccf"
],
[
"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,
"f2aa05bbcb1c5416abe120f3379c07e2"
],
[
"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,
"4b0124a3113b195b5f9f951767b65d56"
],
[
"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,
"9db4a9773d7684362d17ded0c504b8c8"
],
[
"EverCrypt.AEAD.create_in_st",
1,
0,
0,
[ "@query", "projection_inverse_BoxBool_proj_0" ],
0,
"dea1cb524c01fca82c1bdde53dd8e7f2"
],
[
"EverCrypt.AEAD.create_in_chacha20_poly1305",
1,
0,
0,
[ "@query" ],
0,
"0e7963e00f4111277b9b9dc9347d427f"
],
[
"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.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,
"f7f029bc4836a60010c1de864d1814e1"
],
[
"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.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.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key",
"typing_tok_EverCrypt.Error.Success@tok",
"typing_tok_EverCrypt.Error.UnsupportedAlgorithm@tok"
],
0,
"604e999591c2364e80492e3e036d8398"
],
[
"EverCrypt.AEAD.create_in",
1,
0,
0,
[ "@query" ],
0,
"f19ef006f3c4d610efe4d73be794b6ab"
],
[
"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,
"4bb79a484a934cc768fe5231dd025765"
],
[
"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,
"98d6112cf26ce2a070990ca78290e9e2"
],
[
"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,
"077a326a4ddc46fecc3861dccf27954e"
],
[
"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,
"b14c0e500365a4167f0e2e2e0411af52"
],
[
"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.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.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.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.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_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.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,
"f092fcfceca9ec54760c388de2897c25"
],
[
"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,
"8f219eeca0fc2c230508962412e0253c"
],
[
"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,
"c7fdec0ad6f1a1ba5057614f4226f028"
],
[
"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,
"1db0c25f7272720f76eefe60914aaf18"
],
[
"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.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_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.CHACHA20_POLY1305@tok",
"equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.as_kv",
"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.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_nonce",
"equation_Spec.Chacha20Poly1305.aead_encrypt",
"equation_Spec.Chacha20Poly1305.nonce",
"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_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_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_fb77d4109290540100357b20e0a78486",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_kinding_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0",
"typing_EverCrypt.AEAD.as_kv", "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.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,
"a56a20ad629b757fa14b21658c743208"
],
[
"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,
"4902efbad25703c0ee89b9e16dbefbd2"
],
[
"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,
"e6db042de8ccfe8e89ab98c78bdfe751"
],
[
"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.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.decrypted",
"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.max_length",
"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.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.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.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_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_ad8bde7e11e1e3be604a1c227f9bafd7",
"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.mk_mem",
"typing_FStar.Monotonic.HyperStack.pop",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.seq",
"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.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.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,
"9b03c5cb6de7d8ec7a855d347906ae84"
],
[
"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,
"332d3f7b4eb7ef3a54b6b9ea0ed1f13e"
],
[
"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,
"3cbe9f3b9b74af7fa1e1fa3e1ce85401"
],
[
"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,
"d645e5d98a2958322ef548ebc42fa818"
],
[
"EverCrypt.AEAD.decrypt",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"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_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.U128",
"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.CHACHA20_POLY1305",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"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.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.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.U64@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok",
"equation_EverCrypt.AEAD.ad_p", "equation_EverCrypt.AEAD.as_kv",
"equation_EverCrypt.AEAD.cipher_p",
"equation_EverCrypt.AEAD.footprint",
"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.numbytes", "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_Prims.squash",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"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.supported_alg",
"equation_Spec.Agile.AEAD.tag_length",
"equation_Spec.Agile.AEAD.uint8", "equation_Spec.Chacha20.size_key",
"equation_Spec.Chacha20Poly1305.aead_decrypt",
"equation_Spec.Chacha20Poly1305.key",
"equation_Spec.Chacha20Poly1305.size_key",
"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_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_inversion",
"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_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.UInt.pow2_values", "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.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_impl",
"projection_inverse_EverCrypt.AEAD.Ek_kv",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"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_273338279bf37cbeeea1300ffa8034be",
"refinement_interpretation_Tm_refine_295569119c81646492ddb7b407c3c519",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"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_982fb3d3fec67274e50be352a80fb36e",
"refinement_interpretation_Tm_refine_9c278566a1076c216e9de7ddec9e41a6",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9e5d748a0876a43b3055c6e74cacea51",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_ae73b51347bf47c4befe53573dedc34b",
"refinement_interpretation_Tm_refine_bdb8e2f4b5a690ae0ff20fed002844e2",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0",
"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",
"refinement_kinding_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0",
"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.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"
],
0,
"1315012e457346dcbfd00c5605d9814c"
],
[
"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,
"6a5689b21d37a14b9713e79551128411"
]
]
]
Computing file changes ...
