Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
EverCrypt.AEAD.fst.hints
[
"`�)pq��jlj�`���J",
[
[
"EverCrypt.AEAD.uu___0",
1,
0,
0,
[ "@query" ],
0,
"b0fcb793f35baa806a321ed6450501a6"
],
[
"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_FStar.Pervasives.inversion",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.is_supported_alg",
"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_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"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,
"26e8bb20ad00cf8fba16ded70a0b9ba5"
],
[
"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,
"1f847f0568ba86d3906eaf6b8de91e8e"
],
[
"EverCrypt.AEAD.loc_includes_union_l_footprint_s",
1,
0,
0,
[ "@query" ],
0,
"c90e2c52ffb379e59b43674617ad359a"
],
[
"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,
"18a2b47578c3739611b000d8c86b3086"
],
[
"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,
"ba87c2ee25bf21a0cf09e7c476c58759"
],
[
"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,
"8d9faa14157e132e1ccddc820a1f3791"
],
[
"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.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.AEAD.AES128_GCM",
"constructor_distinct_Spec.AEAD.AES256_GCM",
"constructor_distinct_Spec.AEAD.CHACHA20_POLY1305",
"constructor_distinct_Spec.AES.AES128",
"constructor_distinct_Spec.AES.AES256",
"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.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.AEAD.AES128_GCM@tok",
"equality_tok_Spec.AEAD.AES256_GCM@tok",
"equality_tok_Spec.AEAD.CHACHA20_POLY1305@tok",
"equality_tok_Spec.AES.AES128@tok",
"equality_tok_Spec.AES.AES256@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.Pervasives.inversion", "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_Spec.AEAD.cipher_alg_of_supported_alg",
"equation_Spec.AEAD.is_supported_alg",
"equation_Spec.AEAD.key_length", "equation_Spec.AEAD.kv",
"equation_Spec.AEAD.lbytes", "equation_Spec.AEAD.uint8",
"equation_Spec.AES.aes_key", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.AES.key_size",
"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_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_FStar.UInt8.t",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Prims.int",
"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_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e",
"refinement_interpretation_Tm_refine_cb45872aca59bbdc3fe9f2629094edce",
"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.AEAD.is_supported_alg", "typing_Spec.AEAD.kv",
"typing_Spec.AES.gf8",
"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,
"69461c59e1610e78d3bc994745599544"
],
[
"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,
"6f3bcc3bdd67a3755b1d063c29c0cd59"
],
[
"EverCrypt.AEAD.create_in_st",
1,
0,
0,
[ "@query", "projection_inverse_BoxBool_proj_0" ],
0,
"55a2ff613d8ea895d234f1d623f16919"
],
[
"EverCrypt.AEAD.create_in_chacha20_poly1305",
1,
0,
0,
[ "@query" ],
0,
"d186e369b7618332a682eccb07c39e0a"
],
[
"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.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.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.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.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_eternal_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_FStar.UInt8.t",
"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_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_161e04719814801d293219f408210f95",
"refinement_interpretation_Tm_refine_38afdbd936147853b9dadd28b3d45687",
"refinement_interpretation_Tm_refine_3adad2fa15bf57cd1bb4986f7f40a94b",
"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_c6c18a7ceb46d419c35ff8551117551e",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_fe51cca8fdb50c57a53b1f8650a631e6",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"true_interp", "typing_FStar.Map.domain",
"typing_FStar.Monotonic.HyperHeap.color",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.is_eternal_color",
"typing_FStar.Seq.Base.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,
"c981a0fc256047d9c30aa55dbb2d5750"
],
[
"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.W128",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"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.AES.AES128",
"constructor_distinct_Spec.AES.AES256",
"constructor_distinct_Spec.Agile.AEAD.AES128_GCM",
"constructor_distinct_Spec.Agile.AEAD.AES256_GCM",
"constructor_distinct_Spec.Agile.Cipher.AES128",
"constructor_distinct_Spec.Agile.Cipher.AES256",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES128",
"constructor_distinct_Spec.Cipher.Expansion.Vale_AES256",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"equality_tok_EverCrypt.Error.Success@tok",
"equality_tok_EverCrypt.Error.UnsupportedAlgorithm@tok",
"equality_tok_FStar.Integers.W128@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_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",
"equality_tok_Vale.AES.AES_s.AES_128@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.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.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_eternal_color",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Pervasives.inversion", "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.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.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.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",
"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_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_096dcb399122345db27f37346c43e5dc",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_161e04719814801d293219f408210f95",
"refinement_interpretation_Tm_refine_33d23738b4b15f7b09fd193199ac0f72",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_67050f0bec933c5477cc1dda6e0b4da0",
"refinement_interpretation_Tm_refine_6ea4bc7028499f65caa924b56470ac27",
"refinement_interpretation_Tm_refine_779c54d3413fe40c75b3220acf1a3dba",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_8ae37d1557d85b8479513decc054eed2",
"refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e",
"refinement_interpretation_Tm_refine_cbd1f40a916430526e1d584a1995f925",
"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_EverCrypt.CTR.Keys.key_offset", "typing_FStar.Map.domain",
"typing_FStar.Monotonic.HyperHeap.color",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.is_eternal_color",
"typing_FStar.Seq.Base.create", "typing_FStar.Set.singleton",
"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.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.AES.irred",
"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",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"00017050f1558641e3bd9a235171d367"
],
[
"EverCrypt.AEAD.create_in",
1,
0,
0,
[ "@query" ],
0,
"8a19a7338e9e39edfaca74c4dd39a56c"
],
[
"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,
"e98025ffe365bab69dfd105e377c1d1a"
],
[
"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,
"078a334a5b515dc32b9116e51bb14c5c"
],
[
"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,
"2e7fff7d1844b934742269742e16a6aa"
],
[
"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",
"equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat32",
"lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
"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_2a543512a5601f5e6ff9e708bad95df8",
"refinement_interpretation_Tm_refine_ad202434bc72f673ab2665155b0bc87e",
"refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f9bf4b2dbe3e298e2a6f3968d31d88a2",
"typing_EverCrypt.CTR.Keys.vale_alg_of_vale_impl",
"typing_FStar.Ghost.reveal", "typing_FStar.Seq.Base.seq",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"unit_typing"
],
0,
"1a9362354e90e5c9b3e5e24f830797ef"
],
[
"EverCrypt.AEAD.encrypt_aes_gcm",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_EverCrypt.Error.InvalidKey",
"constructor_distinct_EverCrypt.Error.Success",
"constructor_distinct_FStar.Integers.W128",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"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.W128@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.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.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_stack_region",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.Pervasives.inversion",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_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.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_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.max_length",
"equation_Spec.Agile.AEAD.tag_length",
"equation_Spec.Agile.AEAD.uint8",
"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.le_seq_quad32_to_bytes",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"equation_Vale.Def.Words.Seq_s.seq_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.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"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_096dcb399122345db27f37346c43e5dc",
"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_21e94d81ba30d97ef8ce075f9a843f09",
"refinement_interpretation_Tm_refine_352f29f5b291d9b891739cdac915fa8c",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_37e7eb2380b76fa13a43757de3750112",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_42c19092464aa9ffd918cd1331d01085",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_665f89ba62a8e1075fd59aa0042f661f",
"refinement_interpretation_Tm_refine_779c54d3413fe40c75b3220acf1a3dba",
"refinement_interpretation_Tm_refine_79f1f8b4d6774015af27e4432311c913",
"refinement_interpretation_Tm_refine_7c655d1405629ff643b03074f7df95c0",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8d45d8b47d49c79d2c9a76c0f9cd4104",
"refinement_interpretation_Tm_refine_982fb3d3fec67274e50be352a80fb36e",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e",
"refinement_interpretation_Tm_refine_cbd1f40a916430526e1d584a1995f925",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_dd592ff911d0f80cdf0ace6c4224ff73",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"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.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.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.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_def",
"typing_Vale.AES.AES_s.key_to_round_keys_LE",
"typing_Vale.AES.OptPublic.get_hkeys_reqs",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"typing_Vale.Def.Words.Seq_s.seq_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,
"e2f5cca6715e6b2533efe806915ca8f1"
],
[
"EverCrypt.AEAD.encrypt_aes128_gcm",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM",
"equality_tok_Spec.Agile.AEAD.AES128_GCM@tok",
"equation_Spec.Agile.AEAD.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"19b015cd51f6760593380d069522e613"
],
[
"EverCrypt.AEAD.encrypt_aes256_gcm",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.AEAD.AES256_GCM",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.AEAD.AES256_GCM@tok",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"ee75e7214d9af2add7fd1a6c1a41f2e7"
],
[
"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,
"28f20ec238b581037a8d7b20c898efe2"
],
[
"EverCrypt.AEAD.encrypt",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"assumption_FStar.UInt32.t__uu___haseq", "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.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"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_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.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.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.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.mem",
"equation_FStar.Pervasives.inversion", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.eq_or_disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.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.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.pointer_or_null",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.encrypt",
"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.chacha20_encrypt_bytes",
"equation_Spec.Chacha20.counter", "equation_Spec.Chacha20.key",
"equation_Spec.Chacha20.nonce", "equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key",
"equation_Spec.Chacha20.size_nonce",
"equation_Spec.Chacha20Poly1305.aead_encrypt",
"equation_Spec.Chacha20Poly1305.key",
"equation_Spec.Chacha20Poly1305.nonce",
"equation_Spec.Chacha20Poly1305.size_key",
"equation_Spec.Chacha20Poly1305.size_nonce",
"equation_Spec.Cipher.Expansion.concrete_expand",
"equation_Spec.Cipher.Expansion.concrete_xkey_length",
"equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"fuel_guarded_inversion_Spec.Cipher.Expansion.impl",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"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.UInt.pow2_values", "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_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_1a3458802f0c5ea5096a189c5c107fc7",
"refinement_interpretation_Tm_refine_1e64982fd73e0ea5a2ac3364e3b86e76",
"refinement_interpretation_Tm_refine_1f612ea38e642dcb2eb422028ba8b5b6",
"refinement_interpretation_Tm_refine_3e9a939c523db9441d96f9f909e76ac9",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_42c19092464aa9ffd918cd1331d01085",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_5fb3b3eb0d85847dcc819ff24a5d7aa3",
"refinement_interpretation_Tm_refine_615cdbff9e4be4b2687efb17f829c7c1",
"refinement_interpretation_Tm_refine_6ea782d20d3a5b4d53411900c5408b2a",
"refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0",
"refinement_interpretation_Tm_refine_982fb3d3fec67274e50be352a80fb36e",
"refinement_interpretation_Tm_refine_9c278566a1076c216e9de7ddec9e41a6",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_bb420391019b08a67df8b6b95c3fc57c",
"refinement_interpretation_Tm_refine_c5579466c1fcb6457bba4b009a86e2ac",
"refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0",
"refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_dcfcbc0b53101df6437888cfda06bc17",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_de974ede28db942f3b8917b0054bb701",
"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.footprint",
"typing_EverCrypt.AEAD.footprint_s", "typing_FStar.Ghost.reveal",
"typing_FStar.Seq.Base.append", "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.minint", "typing_Lib.IntTypes.unsigned",
"typing_Lib.Sequence.concat", "typing_Lib.Sequence.length",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.g_is_null",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8",
"typing_Spec.Agile.AEAD.kv", "typing_Spec.Chacha20.chacha20_init",
"typing_Spec.Chacha20.chacha20_update",
"typing_Spec.Chacha20.size_block",
"typing_Spec.Chacha20Poly1305.aead_encrypt",
"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,
"5034be9090995dfe0022ac1bd5653ceb"
],
[
"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,
"48d7f359071cf8bc7d37cae4d825f9d8"
],
[
"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_36fd1d0d70eb5e2e645aa7ebf3523b25",
"refinement_interpretation_Tm_refine_3a8538908243c8b50872d962ac5c50b6",
"refinement_interpretation_Tm_refine_595887aa3a4fc1ed355ff0d0cc0cdf2f",
"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,
"6341b692516fad2863249fe56ea70250"
],
[
"EverCrypt.AEAD.decrypt_aes_gcm",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def",
"assumption_FStar.UInt32.t__uu___haseq",
"assumption_FStar.UInt64.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing",
"constructor_distinct_EverCrypt.Error.AuthenticationFailure",
"constructor_distinct_EverCrypt.Error.InvalidKey",
"constructor_distinct_EverCrypt.Error.Success",
"constructor_distinct_FStar.Integers.W128",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"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.W128@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.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.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_stack_region",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.Pervasives.inversion",
"equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_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.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_Spec.AES.aes_key",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.AES.key_size",
"equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg",
"equation_Spec.Agile.AEAD.decrypt",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.Agile.AEAD.iv_length",
"equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.kv",
"equation_Spec.Agile.AEAD.lbytes",
"equation_Spec.Agile.AEAD.max_length",
"equation_Spec.Agile.AEAD.tag_length",
"equation_Spec.Agile.AEAD.uint8",
"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.le_seq_quad32_to_bytes",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"equation_Vale.Def.Words.Seq_s.seq_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.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"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.Seq.Properties.slice_length",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.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_096dcb399122345db27f37346c43e5dc",
"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_21e94d81ba30d97ef8ce075f9a843f09",
"refinement_interpretation_Tm_refine_352f29f5b291d9b891739cdac915fa8c",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_42c19092464aa9ffd918cd1331d01085",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_4a9f5a632ccb67c4adcfd65a1dab0c7c",
"refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_555f3a818a4ea8a3aac7a10eeaddc60a",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_665f89ba62a8e1075fd59aa0042f661f",
"refinement_interpretation_Tm_refine_779c54d3413fe40c75b3220acf1a3dba",
"refinement_interpretation_Tm_refine_79f1f8b4d6774015af27e4432311c913",
"refinement_interpretation_Tm_refine_7c655d1405629ff643b03074f7df95c0",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8f75026f76b9bbf3ca23349b2eb67751",
"refinement_interpretation_Tm_refine_982fb3d3fec67274e50be352a80fb36e",
"refinement_interpretation_Tm_refine_9e5d748a0876a43b3055c6e74cacea51",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e",
"refinement_interpretation_Tm_refine_cbd1f40a916430526e1d584a1995f925",
"refinement_interpretation_Tm_refine_cd18e9962a0d204005dcfcda04529ffc",
"refinement_interpretation_Tm_refine_d0d1d775fb84f5ab7f71a0ac3e01bffa",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_dd592ff911d0f80cdf0ace6c4224ff73",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051",
"refinement_interpretation_Tm_refine_fa18c9f9b58172ff25d6dd8f0d59c16b",
"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.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.append", "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_def",
"typing_Vale.AES.AES_s.key_to_round_keys_LE",
"typing_Vale.AES.OptPublic.get_hkeys_reqs",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"typing_Vale.Def.Words.Seq_s.seq_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_128@tok",
"typing_tok_Vale.AES.AES_s.AES_256@tok"
],
0,
"c3f90fba0be8af36cd0d923d6becfae3"
],
[
"EverCrypt.AEAD.decrypt_aes128_gcm",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM",
"equality_tok_Spec.Agile.AEAD.AES128_GCM@tok",
"equation_Spec.Agile.AEAD.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"1d900f12a4133e7abd868a3d1b59afef"
],
[
"EverCrypt.AEAD.decrypt_aes256_gcm",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.AEAD.AES256_GCM",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.AEAD.AES256_GCM@tok",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"5ace587a61adba3f7288a386089e998d"
],
[
"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,
"c6c7b33bd75cc9bd0b8ebfb2d8464cf5"
],
[
"EverCrypt.AEAD.decrypt",
2,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"assumption_FStar.UInt32.t__uu___haseq", "b2t_def", "bool_inversion",
"bool_typing",
"constructor_distinct_EverCrypt.Error.AuthenticationFailure",
"constructor_distinct_EverCrypt.Error.InvalidKey",
"constructor_distinct_EverCrypt.Error.Success",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"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.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.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.cipher_p",
"equation_EverCrypt.AEAD.footprint",
"equation_EverCrypt.AEAD.footprint_s",
"equation_EverCrypt.AEAD.freeable",
"equation_EverCrypt.AEAD.invariant",
"equation_EverCrypt.AEAD.invariant_s",
"equation_EverCrypt.AEAD.iv_p",
"equation_EverCrypt.AEAD.preserves_freeable",
"equation_EverCrypt.AEAD.state",
"equation_EverCrypt.AEAD.supported_alg_of_impl",
"equation_EverCrypt.CTR.Keys.uint8",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Pervasives.inversion", "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.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.sec_int_t",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.pointer",
"equation_LowStar.Buffer.pointer_or_null",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.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.GaloisField.gf", "equation_Spec.Poly1305.felem",
"equation_Spec.Poly1305.size_key", "equation_Spec.Poly1305.to_felem",
"equation_Spec.Poly1305.zero",
"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",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"inversion-interp", "kinding_EverCrypt.AEAD.state_s@tok",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"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.live_gsub",
"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_gsub_buffer_r_",
"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_liveness_insensitive_buffer_weak",
"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_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_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_42c19092464aa9ffd918cd1331d01085",
"refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_665f89ba62a8e1075fd59aa0042f661f",
"refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
"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_c6c18a7ceb46d419c35ff8551117551e",
"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_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_fa0e7eeef3636052a107ed15123aceaf",
"refinement_interpretation_Tm_refine_fa18c9f9b58172ff25d6dd8f0d59c16b",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_kinding_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0",
"true_interp", "typing_EverCrypt.AEAD.footprint",
"typing_EverCrypt.AEAD.footprint_s", "typing_FStar.Ghost.reveal",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "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.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.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_Spec.Poly1305.zero",
"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,
"ac1ffd82e2a543dfe3b524aeebbe1390"
],
[
"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_FStar.UInt8.t",
"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_9a86663662d48bcd129553a0e1d7e15f",
"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,
"74eeeb5f3bcab1d4fe359e90dc9fc85e"
]
]
]
Computing file changes ...
