Revision 93281362ad4fa0df971a98b303733ad47f7ee0b5 authored by Jonathan Protzenko on 15 April 2020, 18:25:02 UTC, committed by Jonathan Protzenko on 15 April 2020, 18:25:02 UTC
1 parent 321f8c4
Vale.AES.X64.AES256.fsti.hints
[
"8���(�7Khtԋ3��d",
[
[
"Vale.AES.X64.AES256.va_lemma_KeyExpansion256Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Vale.X64.Decls.va_require_total",
"equation_Vale.X64.Decls.validDstAddrs128",
"equation_Vale.X64.Decls.validSrcAddrs128",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_19dcbe503f461f8f8cd69d68660086f5"
],
0,
"72db30c4d4ac57b3cf245e3f48a5130d"
],
[
"Vale.AES.X64.AES256.va_wp_KeyExpansion256Stdcall",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"cbe8ac30f6a5c77859f3c72da3b201db"
],
[
"Vale.AES.X64.AES256.va_quick_KeyExpansion256Stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"f4fd4a60a03ee816402fe8b555a3c25d"
],
[
"Vale.AES.X64.AES256.va_lemma_AES256EncryptBlock",
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_0818b6c65d5ada453a3d58953b442cba"
],
0,
"67223f7af8dd6562dac2e48d532e7eb1"
],
[
"Vale.AES.X64.AES256.va_wp_AES256EncryptBlock",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"2d0967ca1e7506dfbda46e10df01ff67"
],
[
"Vale.AES.X64.AES256.va_quick_AES256EncryptBlock",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"fa39387d5e8a28e4cb4096c901b4bb96"
],
[
"Vale.AES.X64.AES256.va_lemma_AES256EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"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",
"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_4d38686bf695f79f110ce5aef057279f",
"refinement_interpretation_Tm_refine_a725af384906eab1d4c94068c327bac6"
],
0,
"1331743aba3f2e175d3915ba40587fd3"
],
[
"Vale.AES.X64.AES256.va_wp_AES256EncryptBlockStdcall",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"4a3184b0165cd7c84a92c05784c543ca"
],
[
"Vale.AES.X64.AES256.va_quick_AES256EncryptBlockStdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"488210fdeab629d7eb03afc3366e430f"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...