Revision 1068d4afc039dbd12db6dbce298cdb0962d6d224 authored by Aymeric Fromherz on 01 April 2019, 04:39:20 UTC, committed by Aymeric Fromherz on 01 April 2019, 04:39:20 UTC
1 parent d7fe03c
AES_helpers.fst.hints
[
"��=\u0014KRP�Y\u0013��<&��",
[
[
"AES_helpers.expand_key_128_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_e22ba7a032a73f6d0678d3d186686631_1",
"constructor_distinct_AES_s.AES_128", "eq2-interp",
"equality_tok_AES_s.AES_128@tok", "equality_tok_Prims.LexTop@tok",
"equation_AES_s.is_aes_key_LE", "equation_Prims.nat",
"equation_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_ba523126f67e00e7cd55f0b92f16681d",
"well-founded-ordering-on-nat"
],
0,
"3e0faa29891ce678b93cacc70c50f872"
],
[
"AES_helpers.lemma_expand_key_128_0",
1,
4,
0,
[ "@query", "equation_AES_s.nb", "projection_inverse_BoxInt_proj_0" ],
0,
"bf229a0940998736935ae65afa3b1a2a"
],
[
"AES_helpers.lemma_expand_key_128_0",
2,
4,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_AES_s.expand_key_def.fuel_instrumented",
"@fuel_irrelevance_AES_s.expand_key_def.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_AES_s.AES_128", "constructor_distinct_Tm_unit",
"disc_equation_AES_s.AES_128", "disc_equation_AES_s.AES_192",
"disc_equation_AES_s.AES_256", "eq2-interp",
"equality_tok_AES_s.AES_128@tok", "equation_AES_s.aes_key_LE",
"equation_AES_s.expand_key", "equation_AES_s.is_aes_key_LE",
"equation_AES_s.nb", "equation_Prims.nat", "equation_Words_s.nat32",
"equation_with_fuel_AES_s.expand_key_def.fuel_instrumented",
"function_token_typing_Opaque_s.make_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_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_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_76ed5239a4c8f168059df36a5006e0f8",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_e596e646f1b71bf772da1cb0af4e06e9",
"token_correspondence_AES_s.expand_key_def",
"token_correspondence_AES_s.expand_key_def.fuel_instrumented",
"typing_AES_s.expand_key", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_tok_AES_s.AES_128@tok"
],
0,
"78cdf7ca71fcd6c64be7a583927e2741"
],
[
"AES_helpers.lemma_expand_key_128_i",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_AES_s.nb",
"equation_Prims.l_and", "equation_Prims.nat",
"equation_Prims.squash", "equation_Words_s.nat32", "int_inversion",
"l_and-interp", "primitive_Prims.op_LessThan",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0b4a13f44563398bd21134c879b4f4b7",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_974ea6f3ebb2d8e5fd635575758d08ab",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"cd1cf264e55a7fc2b52f5b2044d97138"
],
[
"AES_helpers.lemma_expand_key_128_i",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_AES_s.expand_key_def.fuel_instrumented",
"@fuel_irrelevance_AES_s.expand_key_def.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_AES_s.AES_128", "constructor_distinct_Tm_unit",
"disc_equation_AES_s.AES_128", "disc_equation_AES_s.AES_192",
"disc_equation_AES_s.AES_256", "eq2-interp",
"equality_tok_AES_s.AES_128@tok",
"equation_AES_helpers.round_key_128",
"equation_AES_helpers.round_key_128_rcon",
"equation_AES_s.aes_key_LE", "equation_AES_s.aes_rcon",
"equation_AES_s.expand_key", "equation_AES_s.is_aes_key_LE",
"equation_AES_s.nb", "equation_Prims.nat", "equation_Words_s.nat32",
"equation_Words_s.natN",
"equation_with_fuel_AES_s.expand_key_def.fuel_instrumented",
"function_token_typing_Opaque_s.make_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"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_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_2bf3cadcc460de0bf8493cb981f18e22",
"refinement_interpretation_Tm_refine_31a29d845412f091ee86b3dfb070625b",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_76ed5239a4c8f168059df36a5006e0f8",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a1f2c7ff81ed13f15bce6a9616b67b8f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_ba9a58816d448fc491a61821a10b6b50",
"refinement_interpretation_Tm_refine_e596e646f1b71bf772da1cb0af4e06e9",
"token_correspondence_AES_s.expand_key_def", "typing_AES_s.aes_rcon",
"typing_AES_s.expand_key", "typing_AES_s.rot_word_LE",
"typing_AES_s.sub_word", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Types_s.ixor", "typing_tok_AES_s.AES_128@tok"
],
0,
"09c008a14001bba2f4789c24b56c58c4"
],
[
"AES_helpers.lemma_expand_append",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_AES_s.nb",
"equation_Prims.l_and", "equation_Prims.nat",
"equation_Prims.squash", "equation_Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "l_and-interp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"6590dbd86767e2b4d723ef9f913655b7"
],
[
"AES_helpers.lemma_expand_append",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing", "equation_AES_s.nb",
"equation_Prims.l_and", "equation_Prims.nat",
"equation_Prims.squash", "equation_Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "l_and-interp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"9a81f6da09f3a36d791c69fda80a95c8"
],
[
"AES_helpers.lemma_expand_append",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_AES_s.expand_key_def.fuel_instrumented",
"@fuel_irrelevance_AES_s.expand_key_def.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_e22ba7a032a73f6d0678d3d186686631_1",
"binder_x_e22ba7a032a73f6d0678d3d186686631_2",
"binder_x_f20bacf911070edfdf30866cf54cdf4e_0", "bool_inversion",
"bool_typing", "constructor_distinct_AES_s.AES_128",
"constructor_distinct_Tm_unit", "disc_equation_AES_s.AES_128",
"disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
"eq2-interp", "equality_tok_AES_s.AES_128@tok",
"equality_tok_Prims.LexTop@tok", "equation_AES_s.aes_key_LE",
"equation_AES_s.expand_key", "equation_AES_s.is_aes_key_LE",
"equation_AES_s.nb", "equation_Prims.nat", "equation_Words_s.nat32",
"equation_with_fuel_AES_s.expand_key_def.fuel_instrumented",
"function_token_typing_Opaque_s.make_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"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_GreaterThan",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_76ed5239a4c8f168059df36a5006e0f8",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d0f5986871ea0db2b9870d6e552d5f9b",
"refinement_interpretation_Tm_refine_e596e646f1b71bf772da1cb0af4e06e9",
"token_correspondence_AES_s.expand_key_def", "typing_AES_s.aes_rcon",
"typing_AES_s.expand_key", "typing_AES_s.rot_word_LE",
"typing_AES_s.sub_word", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_Types_s.ixor",
"typing_tok_AES_s.AES_128@tok", "well-founded-ordering-on-nat"
],
0,
"23f6fa4757c28ea74c431977fdc776ef"
],
[
"AES_helpers.lemma_expand_key_128",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_AES_s.nb",
"equation_Prims.l_and", "equation_Prims.nat",
"equation_Prims.squash", "equation_Types_s.quad32",
"equation_Words_s.nat32", "int_inversion", "l_and-interp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_9cb82c4ebe6abcb785bea99f8b687bdd",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"c79a23bf06ee84c8de4e435295c97ecf"
],
[
"AES_helpers.lemma_expand_key_128",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_AES_s.nb",
"equation_Prims.l_and", "equation_Prims.squash",
"equation_Types_s.quad32", "equation_Words_s.nat32", "l_and-interp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_9cb82c4ebe6abcb785bea99f8b687bdd",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
],
0,
"54c56df867ebda32daffbe06645256c4"
],
[
"AES_helpers.lemma_expand_key_128",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_AES_helpers.expand_key_128_def.fuel_instrumented",
"@fuel_correspondence_AES_s.key_schedule_to_round_keys.fuel_instrumented",
"@fuel_irrelevance_AES_helpers.expand_key_128_def.fuel_instrumented",
"@fuel_irrelevance_AES_s.key_schedule_to_round_keys.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_dc562848c16e0cba66fd6b1d2deb3252_0",
"binder_x_e22ba7a032a73f6d0678d3d186686631_1",
"constructor_distinct_AES_s.AES_128",
"data_typing_intro_Words_s.Mkfour@tok", "eq2-interp",
"equality_tok_AES_s.AES_128@tok", "equality_tok_Prims.LexTop@tok",
"equation_AES_helpers.expand_key_128", "equation_AES_s.aes_key_LE",
"equation_AES_s.expand_key", "equation_AES_s.is_aes_key_LE",
"equation_AES_s.nb", "equation_Prims.nat", "equation_Types_s.quad32",
"equation_Words_s.nat32",
"equation_with_fuel_AES_helpers.expand_key_128_def.fuel_instrumented",
"equation_with_fuel_AES_s.key_schedule_to_round_keys.fuel_instrumented",
"function_token_typing_Opaque_s.make_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"kinding_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_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_1595de2a5e95171c9d69194603bbf4d5",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_76ed5239a4c8f168059df36a5006e0f8",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_e596e646f1b71bf772da1cb0af4e06e9",
"token_correspondence_AES_helpers.expand_key_128_def",
"token_correspondence_AES_s.key_schedule_to_round_keys.fuel_instrumented",
"typing_AES_s.expand_key", "typing_AES_s.key_schedule_to_round_keys",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_tok_AES_s.AES_128@tok", "unit_inversion", "unit_typing",
"well-founded-ordering-on-nat"
],
0,
"39ea984b502fd5cad7c2028655a83a71"
],
[
"AES_helpers.lemma_simd_round_key",
1,
3,
3,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"data_elim_Words_s.Mkfour", "equation_AES_helpers.quad32_shl32",
"equation_AES_helpers.round_key_128_rcon",
"equation_AES_helpers.simd_round_key_128", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Types_s.quad32_xor",
"equation_Types_s.quad32_xor_def", "equation_Words_s.nat32",
"fuel_guarded_inversion_Words_s.four",
"function_token_typing_Opaque_s.make_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_typing",
"proj_equation_Words_s.Mkfour_hi3",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"token_correspondence_Types_s.quad32_xor_def",
"typing_AES_helpers.quad32_shl32",
"typing_AES_helpers.round_key_128_rcon", "typing_AES_s.rot_word_LE",
"typing_AES_s.sub_word", "typing_Types_s.ixor",
"typing_Words_s.__proj__Mkfour__item__hi3"
],
0,
"d00a30f0afcaf3a85072cfc08aa24478"
],
[
"AES_helpers.cipher_opaque",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "disc_equation_AES_s.AES_128",
"disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
"fuel_guarded_inversion_AES_s.algorithm"
],
0,
"eb2cb02e4dbf654f829065db6e44f6ce"
],
[
"AES_helpers.init_rounds_opaque",
1,
1,
0,
[ "@query" ],
0,
"dfa0e242ad8443429f85000dd5dbf7a9"
],
[
"AES_helpers.init_rounds_opaque",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_AES_s.rounds.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_AES_helpers.rounds_opaque", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_with_fuel_AES_s.rounds.fuel_instrumented",
"fuel_guarded_inversion_Words_s.four",
"function_token_typing_Opaque_s.make_opaque",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"token_correspondence_AES_s.rounds"
],
0,
"68cad445e97e069331699fd65f72ba94"
],
[
"AES_helpers.finish_cipher",
1,
1,
2,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"8d359b9b39b8b931aedeec3f32ba5c2a"
],
[
"AES_helpers.finish_cipher",
2,
1,
2,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_AES_s.AES_128",
"constructor_distinct_AES_s.AES_192",
"constructor_distinct_AES_s.AES_256", "disc_equation_AES_s.AES_128",
"disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
"equation_AES_helpers.cipher_opaque",
"equation_AES_helpers.rounds_opaque", "equation_AES_s.cipher",
"equation_Prims.nat", "equation_Types_s.quad32",
"equation_Types_s.quad32_xor", "equation_Words_s.nat32",
"fuel_guarded_inversion_AES_s.algorithm",
"fuel_guarded_inversion_Words_s.four",
"function_token_typing_Opaque_s.make_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_typing",
"kinding_Words_s.four@tok", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"token_correspondence_AES_s.cipher",
"token_correspondence_AES_s.rounds",
"typing_AES_helpers.rounds_opaque", "typing_FStar.Seq.Base.index",
"typing_Types_s.quad32_xor"
],
0,
"74aaae05cecf8c62e14211bac4c312de"
],
[
"AES_helpers.finish_cipher_opt",
1,
1,
2,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "eq2-interp",
"equation_Prims.squash",
"function_token_typing_Prims.__cache_version_number__",
"l_and-interp", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"unit_typing"
],
0,
"24d7866e594c91671ab42301864f87c1"
],
[
"AES_helpers.finish_cipher_opt",
2,
1,
2,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"disc_equation_AES_s.AES_128", "disc_equation_AES_s.AES_192",
"disc_equation_AES_s.AES_256", "eq2-interp",
"equation_AES_helpers.cipher_opaque",
"equation_AES_helpers.rounds_opaque", "equation_AES_s.cipher",
"equation_Prims.squash", "equation_Types_s.quad32",
"equation_Words_s.nat32", "fuel_guarded_inversion_AES_s.algorithm",
"fuel_guarded_inversion_Words_s.four",
"function_token_typing_Prims.__cache_version_number__",
"l_and-interp", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"token_correspondence_AES_s.cipher",
"token_correspondence_AES_s.rounds",
"token_correspondence_Opaque_s.make_opaque", "unit_typing"
],
0,
"c907aa07e914a25ecd5d1a537f640ea6"
],
[
"AES_helpers.lemma_add_0x1000000_reverse_mult",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"AES_helpers_interpretation_Tm_arrow_13c4b89a3ebf564b0ebbea44af29d0a4",
"Collections.Seqs_s_interpretation_Tm_arrow_16ef5f8cd579d0100db603308677b251",
"FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"data_typing_intro_Words_s.Mkfour@tok",
"equation_Collections.Seqs_s.reverse_seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Prims.squash",
"equation_Types_s.nat32_to_be_bytes",
"equation_Types_s.reverse_bytes_nat32",
"equation_Types_s.reverse_bytes_nat32_def",
"equation_Words.Four_s.nat_to_four", "equation_Words.Seq_s.seq4",
"equation_Words.Seq_s.seqn", "equation_Words_s.nat32",
"equation_Words_s.nat8", "equation_Words_s.natN",
"fuel_guarded_inversion_Words_s.four",
"function_token_typing_Opaque_s.make_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat8", "int_inversion", "int_typing",
"interpretation_Tm_abs_d7d9aef2471e26f5da24bca7ac42f31e",
"interpretation_Tm_abs_eba68cf47ef8db14a857918bf808fd3d",
"lemma_FStar.Seq.Base.init_index_",
"lemma_FStar.Seq.Base.lemma_init_len",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_hi3",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Words_s.Mkfour_a",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_1bc5c4f392722fe6a26189e86f17c270",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_37e29e1c3dd347eb60f455ae3b4c7ac1",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_69f03d8dd411997bb63279d9bc82f28d",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_9262c905896341cf00109c35624b92a1",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_kinding_Tm_refine_9262c905896341cf00109c35624b92a1",
"token_correspondence_Opaque_s.make_opaque",
"token_correspondence_Types_s.reverse_bytes_nat32_def",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Tm_abs_ae6a984e63d148c37929f28597b3ef6c",
"typing_Tm_abs_d7d9aef2471e26f5da24bca7ac42f31e",
"typing_Words.Seq_s.four_to_seq_BE", "typing_Words_s.int_to_natN",
"unit_typing"
],
0,
"99eb7c07b6b06ad1b9e4e8a54a65e846"
],
[
"AES_helpers.lemma_incr_msb",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"3adfc3cee84452f46e32ef13effcb630"
],
[
"AES_helpers.lemma_incr_msb",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Arch.Types.add_wrap_quad32", "equation_GCTR_s.inc32",
"equation_Prims.nat", "equation_Types_s.add_wrap",
"equation_Types_s.quad32", "equation_Words.Four_s.four_reverse",
"equation_Words_s.nat32", "equation_Words_s.natN",
"fuel_guarded_inversion_Words_s.four",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"primitive_Prims.op_LessThan", "proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_hi3",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Types_s.reverse_bytes_nat32",
"typing_Words_s.__proj__Mkfour__item__hi2",
"typing_Words_s.__proj__Mkfour__item__hi3",
"typing_Words_s.__proj__Mkfour__item__lo0",
"typing_Words_s.__proj__Mkfour__item__lo1"
],
0,
"be787634b02e4e14192bf6db5a5f3243"
],
[
"AES_helpers.lemma_msb_in_bounds",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Arch.Types.add_wrap_quad32", "equation_GCTR_s.inc32",
"equation_Prims.nat", "equation_Types_s.add_wrap",
"equation_Types_s.quad32", "equation_Words.Four_s.four_reverse",
"equation_Words_s.nat32", "equation_Words_s.natN",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"primitive_Prims.op_LessThan", "proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_hi3",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Types_s.reverse_bytes_nat32",
"typing_Words_s.__proj__Mkfour__item__hi2",
"typing_Words_s.__proj__Mkfour__item__hi3",
"typing_Words_s.__proj__Mkfour__item__lo0",
"typing_Words_s.__proj__Mkfour__item__lo1"
],
0,
"7ecacd986dd1744ce9c978824bfb69bd"
]
]
]
Computing file changes ...
