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.X64.AES128.fsti.hints
[
"�+�6�<�5�\u001fvj\u0019�2o",
[
[
"Vale.AES.X64.AES128.va_lemma_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "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",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"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.Decls.validDstAddrs128",
"equation_Vale.X64.Decls.validSrcAddrs128",
"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",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"refinement_interpretation_Tm_refine_1786c28ad96fef48f93b504abba67154",
"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.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"d6f664067906f09d5016af56b293d024"
],
[
"Vale.AES.X64.AES128.va_wp_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"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.Arch.HeapImpl.vale_heap_impl",
"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.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",
"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.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"03530f4126c91f5ee75fc991387cee95"
],
[
"Vale.AES.X64.AES128.va_quick_KeyExpansion128Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"c8ad1f6d2b146dbef518ff62d05a1518"
],
[
"Vale.AES.X64.AES128.va_lemma_AES128EncryptBlock",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"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_545a5792d0d1eb1563d46f99a317d4bc"
],
0,
"a9ea8e768b176190cfc7026d93ec38fd"
],
[
"Vale.AES.X64.AES128.va_wp_AES128EncryptBlock",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"b7efd8381d48250e6319e88ce420c526"
],
[
"Vale.AES.X64.AES128.va_quick_AES128EncryptBlock",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"2a8aad2412beeae6e238cdce1ecd3258"
],
[
"Vale.AES.X64.AES128.va_lemma_AES128EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.X64.Decls.va_int_range",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.validDstAddrs128",
"equation_Vale.X64.Decls.validSrcAddrs128",
"equation_Vale.X64.Memory.get_vale_heap",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_4d38686bf695f79f110ce5aef057279f",
"refinement_interpretation_Tm_refine_4e67b1b2b736c17ee75eab615881e51b"
],
0,
"d325b1c14d28f52cfe0cf39f8b4a2309"
],
[
"Vale.AES.X64.AES128.va_wp_AES128EncryptBlockStdcall",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"4859b5c6aca33de5290f645c6493956e"
],
[
"Vale.AES.X64.AES128.va_quick_AES128EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"3f2d6ea636aa6e292de4d9f9ba5328cc"
]
]
]
Computing file changes ...
