Revision aa211c2d5a40dd6969fe8a469fcadfd27e8c8fe3 authored by Jonathan Protzenko on 24 April 2020, 21:11:09 UTC, committed by Jonathan Protzenko on 24 April 2020, 21:11:09 UTC
1 parent 6f91754
Vale.AES.X64.AES.fsti.hints
[
"��bj��}h\u0003��;p\u0006",
[
[
"Vale.AES.X64.AES.va_req_KeyExpansionStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"equation_Prims.l_and", "equation_Prims.squash",
"equation_Prims.subtype_of",
"l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"unit_typing"
],
0,
"a0b941b2f559d30bc53fb3f36ed1c97c"
],
[
"Vale.AES.X64.AES.va_ens_KeyExpansionStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
"bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.l_and", "equation_Prims.squash",
"equation_Prims.subtype_of", "equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.X64.AES.va_req_KeyExpansionStdcall",
"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",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
"l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
"primitive_Prims.op_Equality",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.Memory.get_vale_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_tok_Vale.AES.AES_s.AES_128@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "unit_typing"
],
0,
"22174f1b0e3655e490faf8681bbc8f4b"
],
[
"Vale.AES.X64.AES.va_lemma_KeyExpansionStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
"bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"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",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
"primitive_Prims.op_Equality",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_fbf0120317c1791ec21c0732ca73adf7",
"typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.Memory.get_vale_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_tok_Vale.AES.AES_s.AES_128@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"1b4573282d36fd9a699f7391e54de9f4"
],
[
"Vale.AES.X64.AES.va_wp_KeyExpansionStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
"bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"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", "equation_Vale.X64.Decls.va_if",
"equation_Vale.X64.Decls.va_upd_flags",
"equation_Vale.X64.Decls.va_upd_mem",
"equation_Vale.X64.Decls.va_upd_mem_heaplet",
"equation_Vale.X64.Decls.va_upd_mem_layout",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_reg_64",
"equation_Vale.X64.State.update_reg_xmm",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
"interpretation_Tm_abs_38d7eff540413c1542680da4920eb610",
"interpretation_Tm_abs_b56408d008c29abd8498b9b17febc53e",
"primitive_Prims.op_Equality",
"proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_ok",
"refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_c7ddb114a835e1819499f5805e85b51d",
"typing_Vale.AES.AES256_helpers.make_AES256_key",
"typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.Memory.get_vale_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok",
"typing_tok_Vale.AES.AES_s.AES_128@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"3312eb83cb4f7e1d18bdddd9aa7480c9"
],
[
"Vale.AES.X64.AES.va_quick_KeyExpansionStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"57120aee779e368bfe807f78b4dd0f46"
],
[
"Vale.AES.X64.AES.va_lemma_AESEncryptBlock",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.X64.Decls.va_require_total",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_64a90b72eab8ec88bdd5838bbce5e2d0"
],
0,
"2335c5000cce8f43f2741485587413e0"
],
[
"Vale.AES.X64.AES.va_wp_AESEncryptBlock",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"41e05a8773e752671c86548c4a5fd82e"
],
[
"Vale.AES.X64.AES.va_quick_AESEncryptBlock",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"30dcef4cf9042e3da2fd3e5a340a1bb2"
]
]
]
Computing file changes ...
