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.AES256_helpers.fst.hints
[
"�\b���:��v\u0004\u0003�4&JN",
[
[
"Vale.AES.AES256_helpers.make_AES256_key",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
"equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_FStar.Seq.Base.length",
"typing_Vale.Def.Words.Seq_s.four_to_seq_LE"
],
0,
"acdf10c06e7aa209126bd090f0217489"
],
[
"Vale.AES.AES256_helpers.expand_key_256_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Types_s.quad32",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"eb13af7a802615933baa40a1828e0d6f"
],
[
"Vale.AES.AES256_helpers.lemma_reveal_expand_key_256",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.AES256_helpers.expand_key_256_def.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.AES256_helpers.expand_key_256_def.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Vale.AES.AES_s.AES_256", "eq2-interp",
"equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
"equation_Vale.AES.AES256_helpers.expand_key_256",
"equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_with_fuel_Vale.AES.AES256_helpers.expand_key_256_def.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"int_inversion", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"token_correspondence_Vale.AES.AES256_helpers.expand_key_256_def"
],
0,
"75c3632f708759920897f60479a467d6"
],
[
"Vale.AES.AES256_helpers.lemma_expand_key_256_0",
1,
8,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.AES_s.expand_key_def.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.AES_s.expand_key_def.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"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",
"equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
"equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.AES_s.expand_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.AES_s.nb", "equation_Vale.Def.Words_s.nat32",
"equation_with_fuel_Vale.AES.AES_s.expand_key_def.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e69eda982f72ce3ed022c485bb2fc82",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"refinement_interpretation_Tm_refine_86c893bd73295cad27c95bea9e692abe",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_Vale.AES.AES_s.expand_key_def",
"token_correspondence_Vale.AES.AES_s.expand_key_def.fuel_instrumented",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_Vale.AES.AES_s.expand_key",
"typing_tok_Vale.AES.AES_s.AES_256@tok"
],
0,
"446f3a058c6644b1d1d66ea244e0426d"
],
[
"Vale.AES.AES256_helpers.lemma_expand_key_256_i",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.AES_s.expand_key_def.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.AES_s.expand_key_def.fuel_instrumented",
"@query",
"FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"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",
"equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.l_and",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AES.AES256_helpers.round_key_256",
"equation_Vale.AES.AES256_helpers.round_key_256_rcon",
"equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.AES_s.aes_rcon",
"equation_Vale.AES.AES_s.expand_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.AES_s.nb", "equation_Vale.Def.Words_s.nat32",
"equation_Vale.Def.Words_s.natN",
"equation_with_fuel_Vale.AES.AES_s.expand_key_def.fuel_instrumented",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_len_append", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_0c64db7278cf5901caab9642295387c0",
"refinement_interpretation_Tm_refine_2155430dbdfe2cbb2dc939fe5c160cbb",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_3541a3cc1131de1e3a1aac5a3c02ea30",
"refinement_interpretation_Tm_refine_40578c0cab8433f28d34f2cbea32986e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e69eda982f72ce3ed022c485bb2fc82",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"refinement_interpretation_Tm_refine_86c893bd73295cad27c95bea9e692abe",
"refinement_interpretation_Tm_refine_96884e177dd23a2209d073a3fa11b201",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c1b1024e28776cd81d3423da5c72fdff",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_dd779be6e41e6ff5f3aa06cf49e7d775",
"refinement_interpretation_Tm_refine_e85fa1b41e817d8f8a8bbca76c5f0be7",
"token_correspondence_Vale.AES.AES_s.expand_key_def",
"token_correspondence_Vale.AES.AES_s.expand_key_def.fuel_instrumented",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_Vale.AES.AES_s.aes_rcon",
"typing_Vale.AES.AES_s.expand_key",
"typing_Vale.AES.AES_s.rot_word_LE",
"typing_Vale.AES.AES_s.sub_word", "typing_Vale.Def.Types_s.ixor",
"typing_tok_Vale.AES.AES_s.AES_256@tok"
],
0,
"dae47e59a5c2ca90b08f268fb0615499"
],
[
"Vale.AES.AES256_helpers.lemma_expand_append",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AES.AES_s.nb", "int_inversion", "l_and-interp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_86c893bd73295cad27c95bea9e692abe"
],
0,
"3c3f4002d87fff63c76acd2a44d7def0"
],
[
"Vale.AES.AES256_helpers.lemma_expand_append",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.AES_s.expand_key_def.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.AES_s.expand_key_def.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"b2t_def", "binder_x_a5cfac8aaadefcd9e30621ba558d29cf_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "bool_inversion",
"bool_typing", "constructor_distinct_Tm_unit",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"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",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.l_and",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.AES_s.expand_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.AES_s.nb", "equation_Vale.Def.Words_s.nat32",
"equation_with_fuel_Vale.AES.AES_s.expand_key_def.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "l_and-interp", "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_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0b7d6771be1af656c175811639ed9343",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e69eda982f72ce3ed022c485bb2fc82",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_86c893bd73295cad27c95bea9e692abe",
"refinement_interpretation_Tm_refine_9c9f4c90d5c9fbc2be7a6474a8ed2fe5",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_Vale.AES.AES_s.expand_key_def",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_Vale.AES.AES_s.aes_rcon", "typing_Vale.AES.AES_s.expand_key",
"typing_Vale.AES.AES_s.rot_word_LE",
"typing_Vale.AES.AES_s.sub_word", "typing_Vale.Def.Types_s.ixor",
"typing_tok_Vale.AES.AES_s.AES_256@tok",
"well-founded-ordering-on-nat"
],
0,
"18a437b736292a5f0d806aa59e9edba8"
],
[
"Vale.AES.AES256_helpers.lemma_expand_key_256",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AES.AES_s.nb", "int_inversion", "l_and-interp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_501d12a9a3db14d8c73522605e3edbff",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9c2d74ae21ebe21dc37eb1ac96ddb62a"
],
0,
"020645ade464c837c5f050eb057456c3"
],
[
"Vale.AES.AES256_helpers.lemma_expand_key_256",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.l_and",
"equation_Prims.squash", "equation_Vale.AES.AES_s.nb",
"l_and-interp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_501d12a9a3db14d8c73522605e3edbff",
"refinement_interpretation_Tm_refine_9c2d74ae21ebe21dc37eb1ac96ddb62a"
],
0,
"9c19414a699fe2b2be3be32b0b430cb9"
],
[
"Vale.AES.AES256_helpers.lemma_expand_key_256",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.AES.AES_s.key_schedule_to_round_keys.fuel_instrumented",
"@fuel_irrelevance_Vale.AES.AES_s.key_schedule_to_round_keys.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_053894aba25fdc4e0df122563ef9b6f4_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "eq2-interp",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Prims.nat",
"equation_Vale.AES.AES256_helpers.expand_key_256",
"equation_Vale.AES.AES256_helpers.round_key_256",
"equation_Vale.AES.AES256_helpers.round_key_256_rcon",
"equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.AES_s.aes_rcon",
"equation_Vale.AES.AES_s.expand_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.AES_s.nb", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_with_fuel_Vale.AES.AES_s.key_schedule_to_round_keys.fuel_instrumented",
"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_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_492bc8822bd3ab3615cbddc21f2b2327",
"refinement_interpretation_Tm_refine_49e3dffff236adc353edb6005733b1bd",
"refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e69eda982f72ce3ed022c485bb2fc82",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_86c893bd73295cad27c95bea9e692abe",
"refinement_interpretation_Tm_refine_9c2d74ae21ebe21dc37eb1ac96ddb62a",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_Vale.AES.AES_s.key_schedule_to_round_keys.fuel_instrumented",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_Vale.AES.AES256_helpers.expand_key_256",
"typing_Vale.AES.AES_s.expand_key",
"typing_Vale.AES.AES_s.key_schedule_to_round_keys",
"typing_tok_Vale.AES.AES_s.AES_256@tok", "unit_inversion",
"unit_typing", "well-founded-ordering-on-nat"
],
0,
"bffe797e6e73dc428f871ccdaf1efd50"
],
[
"Vale.AES.AES256_helpers.lemma_simd_round_key",
1,
3,
3,
[
"@MaxIFuel_assumption", "@query",
"data_elim_Vale.Def.Words_s.Mkfour", "equation_Prims.nat",
"equation_Vale.AES.AES256_helpers.quad32_shl32",
"equation_Vale.AES.AES256_helpers.round_key_256_rcon",
"equation_Vale.AES.AES256_helpers.simd_round_key_256",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Types_s.quad32_xor",
"equation_Vale.Def.Types_s.quad32_xor_def",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Def.Types_s.quad32_xor_def",
"typing_Vale.AES.AES256_helpers.quad32_shl32",
"typing_Vale.AES.AES256_helpers.round_key_256_rcon",
"typing_Vale.AES.AES_s.rot_word_LE",
"typing_Vale.AES.AES_s.sub_word", "typing_Vale.Def.Types_s.ixor",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3"
],
0,
"93310edd299443df673cf29c2a2661a8"
],
[
"Vale.AES.AES256_helpers.lemma_round_key_256_rcon_odd",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Vale.AES.AES256_helpers.round_key_256_rcon",
"function_token_typing_Prims.__cache_version_number__",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"4180c0675049150e51ec891446a90c1a"
]
]
]
Computing file changes ...
