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
Vale.AES.AES_s.fst.hints
[
"*e\u0003\u001e�<�r���]�M��",
[
[
"Vale.AES.AES_s.nk",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256",
"fuel_guarded_inversion_Vale.AES.AES_s.algorithm"
],
0,
"ddfcf04c9dba7e0e73c66756835ff064"
],
[
"Vale.AES.AES_s.nr",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256",
"fuel_guarded_inversion_Vale.AES.AES_s.algorithm"
],
0,
"69d2dbbaa531e58eac3cabd26245f5ba"
],
[
"Vale.AES.AES_s.aes_key_LE",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Seq.Base.seq__uu___haseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat32",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"8b44e1d266c54a700f0c1ddc31a55f00"
],
[
"Vale.AES.AES_s.aes_key",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Seq.Base.seq__uu___haseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat8",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"1b639d7c6124293c6c920c9c99606f01"
],
[
"Vale.AES.AES_s.rounds",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"binder_x_1bf7805dca102a20dd4cf40ee0e4c344_2",
"binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_1",
"binder_x_e97427d583e1f4d42a96b4bdd8dae147_0",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four", "int_inversion",
"int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_315a550f138cfdf4055c9a83a4f16559",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"d131697f2fc55d157ebac5d8f4fb71dc"
],
[
"Vale.AES.AES_s.cipher",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_Vale.AES.AES_s.algorithm",
"projection_inverse_BoxInt_proj_0"
],
0,
"a102437d8623514af1f0ca92ab34b067"
],
[
"Vale.AES.AES_s.expand_key_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Tm_unit",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256", "eq2-interp",
"equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"typing_FStar.Seq.Base.length"
],
0,
"5dac04d5ff54296f9187de3a85cbde0f"
],
[
"Vale.AES.AES_s.expand_key_def",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
"binder_x_67f87028e6cd57438f0518e237aba197_1",
"binder_x_6e081d3fd4c7d96421c0174a146dcfd4_2",
"constructor_distinct_Tm_unit", "eq2-interp",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.AES.AES_s.AES_128@tok", "equation_Prims.nat",
"equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_11cdebb45c0a0cca398f44b5f50276f4",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_645bb40e871de78b92ef1e26057bb07f",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"refinement_interpretation_Tm_refine_b112e58e47b3662e31627d314f992310",
"typing_FStar.Seq.Base.length",
"typing_tok_Vale.AES.AES_s.AES_128@tok",
"well-founded-ordering-on-nat"
],
0,
"294a386a2dcfd2ee78360130755ededd"
],
[
"Vale.AES.AES_s.expand_key_def",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Tm_unit",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256", "eq2-interp",
"equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"typing_FStar.Seq.Base.length"
],
0,
"114b667bf1990dda8b3c6a927db82db3"
],
[
"Vale.AES.AES_s.expand_key",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Tm_unit",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256", "eq2-interp",
"equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"typing_FStar.Seq.Base.length"
],
0,
"9bb1a6aa2167414570fe54ca00ee75b1"
],
[
"Vale.AES.AES_s.key_schedule_to_round_keys",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_d7643cb47c00f184cbfede60aad14863_1", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_56fce1a01658afc5bf5db7dd799c58ab",
"refinement_interpretation_Tm_refine_8675e80e2a8f9bda5210205b84b7bbbb",
"typing_FStar.Seq.Base.create", "well-founded-ordering-on-nat"
],
0,
"9e91105225a3c46e1fac58b2ab66abfe"
],
[
"Vale.AES.AES_s.key_to_round_keys_LE",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"eq2-interp", "equation_Prims.nat",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.AES_s.nb", "equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6111c4f6a61843caee0d07c84de0edb2",
"refinement_interpretation_Tm_refine_dd592ff911d0f80cdf0ace6c4224ff73",
"typing_FStar.Seq.Base.length"
],
0,
"4c2a9bc0939a4e34cb175b37540251c1"
],
[
"Vale.AES.AES_s.aes_encrypt_LE_def",
1,
1,
0,
[ "@query" ],
0,
"d824739f8539e9122347faa7ed033420"
],
[
"Vale.AES.AES_s.key_to_round_keys",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Vale.AES.AES_s.AES_128", "eq2-interp",
"equation_Vale.AES.AES_s.aes_key",
"equation_Vale.AES.AES_s.is_aes_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"fuel_guarded_inversion_Vale.AES.AES_s.algorithm",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c2a75a3c0618fe8966569957451b4eb6",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
],
0,
"d2fbfee6bc931683bcb19c531e3c54b2"
],
[
"Vale.AES.AES_s.aes_encrypt",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
"equation_Vale.AES.AES_s.aes_key",
"equation_Vale.AES.AES_s.is_aes_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words.Seq_s.seq16",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"fuel_guarded_inversion_Vale.AES.AES_s.algorithm",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_init_len",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c2a75a3c0618fe8966569957451b4eb6",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
],
0,
"656df5cae06ad3a226c77b08098afc13"
],
[
"Vale.AES.AES_s.nk",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256",
"fuel_guarded_inversion_Vale.AES.AES_s.algorithm"
],
0,
"6a1948b0201aa89cef13803b68b1f350"
],
[
"Vale.AES.AES_s.nr",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256",
"fuel_guarded_inversion_Vale.AES.AES_s.algorithm"
],
0,
"658bef5217f5615f82c86ebf34289714"
],
[
"Vale.AES.AES_s.aes_key_LE",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Seq.Base.seq__uu___haseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat32",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"fe346c31c8c6f4fb94924a13e65864cc"
],
[
"Vale.AES.AES_s.aes_key",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Seq.Base.seq__uu___haseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat8",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"99c11688f64d042277a75395426199d7"
],
[
"Vale.AES.AES_s.rounds",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"binder_x_1bf7805dca102a20dd4cf40ee0e4c344_2",
"binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_1",
"binder_x_e97427d583e1f4d42a96b4bdd8dae147_0",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four", "int_inversion",
"int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_315a550f138cfdf4055c9a83a4f16559",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"af437d316ee969fc7a7d4d6e5c256a4e"
],
[
"Vale.AES.AES_s.cipher",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_Vale.AES.AES_s.algorithm",
"projection_inverse_BoxInt_proj_0"
],
0,
"07a6339f39d2d45eb3b272d07069569a"
],
[
"Vale.AES.AES_s.cipher",
3,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256",
"fuel_guarded_inversion_Vale.AES.AES_s.algorithm"
],
0,
"ec361a30ef7fe14515679b89f8eea3c1"
],
[
"Vale.AES.AES_s.expand_key_def",
4,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Tm_unit",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256", "eq2-interp",
"equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"typing_FStar.Seq.Base.length"
],
0,
"8f381f7cbee8bccadaf022b8002abe6d"
],
[
"Vale.AES.AES_s.expand_key_def",
5,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
"binder_x_67f87028e6cd57438f0518e237aba197_1",
"binder_x_6e081d3fd4c7d96421c0174a146dcfd4_2",
"constructor_distinct_Tm_unit", "eq2-interp",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.AES.AES_s.AES_128@tok", "equation_Prims.nat",
"equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_11cdebb45c0a0cca398f44b5f50276f4",
"refinement_interpretation_Tm_refine_4d15538b13414facf55da6b5ea0cd679",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"refinement_interpretation_Tm_refine_b112e58e47b3662e31627d314f992310",
"typing_FStar.Seq.Base.length",
"typing_tok_Vale.AES.AES_s.AES_128@tok",
"well-founded-ordering-on-nat"
],
0,
"d7b2bbe34c01b94c904e947e7f67f070"
],
[
"Vale.AES.AES_s.expand_key_def",
6,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Tm_unit",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256", "eq2-interp",
"equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"typing_FStar.Seq.Base.length"
],
0,
"c3fc04ad56150a7ae3d401cef52a0b32"
],
[
"Vale.AES.AES_s.expand_key",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Tm_unit",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256", "eq2-interp",
"equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"typing_FStar.Seq.Base.length"
],
0,
"05790ad88a26c0a3a62662d1c2b550ee"
],
[
"Vale.AES.AES_s.key_schedule_to_round_keys",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_d7643cb47c00f184cbfede60aad14863_1", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_56fce1a01658afc5bf5db7dd799c58ab",
"refinement_interpretation_Tm_refine_8675e80e2a8f9bda5210205b84b7bbbb",
"typing_FStar.Seq.Base.create", "well-founded-ordering-on-nat"
],
0,
"5d38d4a8c3ee3ffcab22b25408643d8b"
],
[
"Vale.AES.AES_s.key_to_round_keys_LE",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Tm_unit", "eq2-interp", "equation_Prims.nat",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.AES_s.nb", "equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6111c4f6a61843caee0d07c84de0edb2",
"refinement_interpretation_Tm_refine_dd592ff911d0f80cdf0ace6c4224ff73",
"typing_FStar.Seq.Base.length"
],
0,
"1c93c0549800031c3072b27d88390c2f"
],
[
"Vale.AES.AES_s.key_to_round_keys_LE",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Tm_unit",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256", "eq2-interp",
"equation_Prims.nat", "equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ec4cc42b2040d52d9e001ddd04314ad8",
"typing_FStar.Seq.Base.length"
],
0,
"6b15c7940542c37a293873933750bed6"
],
[
"Vale.AES.AES_s.aes_encrypt_LE_def",
2,
1,
0,
[ "@query" ],
0,
"e7c6904336447f414b8f17f45dc9af38"
],
[
"Vale.AES.AES_s.key_to_round_keys",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Vale.AES.AES_s.AES_128", "eq2-interp",
"equation_Vale.AES.AES_s.aes_key",
"equation_Vale.AES.AES_s.is_aes_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"fuel_guarded_inversion_Vale.AES.AES_s.algorithm",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c2a75a3c0618fe8966569957451b4eb6",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
],
0,
"ecbe3d003d852b2cbd7c738f1930ab2f"
],
[
"Vale.AES.AES_s.key_to_round_keys",
3,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.AES.AES_s.AES_128",
"disc_equation_Vale.AES.AES_s.AES_192",
"disc_equation_Vale.AES.AES_s.AES_256",
"fuel_guarded_inversion_Vale.AES.AES_s.algorithm"
],
0,
"772661ca0d6087af303c27a25103c873"
],
[
"Vale.AES.AES_s.aes_encrypt",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
"equation_Vale.AES.AES_s.aes_key",
"equation_Vale.AES.AES_s.is_aes_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Words.Seq_s.seq16",
"equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"fuel_guarded_inversion_Vale.AES.AES_s.algorithm",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_init_len",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
"refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c2a75a3c0618fe8966569957451b4eb6",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
"typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
],
0,
"9a4cc6d2fea845206cdaba2ad97664f0"
]
]
]
Computing file changes ...
