Revision 0d9153dc34ee2dcf0821e3f21e825fc5bb8895b4 authored by Santiago Zanella-Beguelin on 11 December 2019, 17:46:08 UTC, committed by Santiago Zanella-Beguelin on 12 December 2019, 10:33:01 UTC
1 parent 7405f78
EverCrypt.CTR.Keys.fst.hints
[
"H�\u000e�ӊ�\u0015L ���/�U",
[
[
"EverCrypt.CTR.Keys.uu___0",
1,
0,
0,
[ "@query" ],
0,
"56cb47a58bc7ae39855d0095fc00d1b0"
],
[
"EverCrypt.CTR.Keys.vale_impl",
1,
0,
0,
[ "@query", "assumption_Spec.Cipher.Expansion.impl__uu___haseq" ],
0,
"6789fc7c331a72aa23bc082a041d3827"
],
[
"EverCrypt.CTR.Keys.vale_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,
"1683bb6e6f7f77a9adeea8c00a484be4"
],
[
"EverCrypt.CTR.Keys.key_offset",
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_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_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",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35",
"typing_EverCrypt.CTR.Keys.vale_alg_of_vale_impl", "unit_typing"
],
0,
"9570dc3296812bc22ee98585e8404f97"
],
[
"EverCrypt.CTR.Keys.concrete_xkey_len",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"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",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"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.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@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_256@tok",
"equation_EverCrypt.CTR.Keys.key_offset",
"equation_EverCrypt.CTR.Keys.vale_alg_of_vale_impl",
"equation_FStar.Integers.int_t",
"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.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_key",
"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",
"fuel_guarded_inversion_Spec.Cipher.Expansion.impl", "int_typing",
"inversion-interp", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.vu_inv", "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_096dcb399122345db27f37346c43e5dc",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_55d0e7c52739a80eaeffbef97124b643",
"refinement_interpretation_Tm_refine_779c54d3413fe40c75b3220acf1a3dba",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.add",
"typing_FStar.UInt32.v", "typing_Lib.IntTypes.v",
"typing_Spec.AES.gf8", "typing_Spec.AES.irred",
"typing_Spec.Chacha20.size_key",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"b7dffaa0150c1d24b83788b8381795d1"
],
[
"EverCrypt.CTR.Keys.aes_gcm_key_expansion",
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.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_47c38a2667c0257615c47d5f0154302e",
"refinement_interpretation_Tm_refine_81279e0044965bd29b2ae1ad50881142",
"refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35",
"refinement_interpretation_Tm_refine_d116e5eae57261debae86fed213a8efe",
"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,
"c423910ceadb0fcc702643bea6426485"
],
[
"EverCrypt.CTR.Keys.aes_gcm_keyhash_init",
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_9615a4c904197e4feb6d5e24601cdce3",
"refinement_interpretation_Tm_refine_c029c44ff4b4f840d75208dea95cad35",
"refinement_interpretation_Tm_refine_d0e476e8e1298c5970de46fcd46735ea",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f3cbc636e9903d9abfe39996434c29ca",
"typing_EverCrypt.CTR.Keys.vale_alg_of_vale_impl",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"unit_typing"
],
0,
"85d9de78deaaf81891ba88d2a277b52c"
],
[
"EverCrypt.CTR.Keys.vale_expand",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Def.Words.Two_s_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_FStar.Integers.W128",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.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.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_FStar.Integers.W128@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@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.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.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.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.size_t", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AES.aes_key",
"equation_Spec.AES.elem", "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_aes_expansion",
"equation_Spec.Cipher.Expansion.vale_alg_of_cipher_alg",
"equation_Spec.Cipher.Expansion.vale_xkey_length",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Vale.AES.AES_s.is_aes_key_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_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.X64.CPU_Features_s.sse_enabled",
"fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg",
"fuel_guarded_inversion_Spec.Cipher.Expansion.impl",
"function_token_typing_Lib.IntTypes.byte_t",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_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_Vale.Def.Words_s.four@tok",
"lemma_FStar.Ghost.reveal_hide",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"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.UInt32.vu_inv",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_uint8_to_seq_nat8",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "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_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_22031f78f7e45c35d05f7046cff619c6",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
"refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_779c54d3413fe40c75b3220acf1a3dba",
"refinement_interpretation_Tm_refine_79f1f8b4d6774015af27e4432311c913",
"refinement_interpretation_Tm_refine_7a82ef654f8b681bd9a3571401dece6c",
"refinement_interpretation_Tm_refine_81279e0044965bd29b2ae1ad50881142",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"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_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",
"true_interp", "typing_EverCrypt.CTR.Keys.concrete_xkey_len",
"typing_EverCrypt.CTR.Keys.key_offset",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.seq", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.length",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.mgsub", "typing_Spec.AES.gf8",
"typing_Spec.Agile.Cipher.key",
"typing_Spec.Cipher.Expansion.cipher_alg_of_impl",
"typing_Spec.Cipher.Expansion.concrete_expand",
"typing_Spec.Cipher.Expansion.concrete_xkey_length",
"typing_Spec.GaloisField.__proj__GF__item__t",
"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_nat32_LE",
"typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
"typing_Vale.X64.CPU_Features_s.aesni_enabled",
"typing_Vale.X64.CPU_Features_s.avx_enabled",
"typing_Vale.X64.CPU_Features_s.sse4_1_enabled",
"typing_Vale.X64.CPU_Features_s.sse_enabled",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok",
"typing_tok_Spec.Cipher.Expansion.Vale_AES128@tok",
"typing_tok_Spec.Cipher.Expansion.Vale_AES256@tok",
"typing_tok_Vale.AES.AES_s.AES_128@tok",
"typing_tok_Vale.AES.AES_s.AES_256@tok"
],
0,
"ac04670080e875243b548973d5fc2296"
]
]
]
Computing file changes ...
