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.AESCTR.fsti.hints
[
"\u0012�M�i\\�\u0017�WO���,\u007f",
[
[
"Vale.AES.X64.AESCTR.aes_reqs",
1,
1,
0,
[ "@query" ],
0,
"750f1d0e197e0a9e34186c63228aa840"
],
[
"Vale.AES.X64.AESCTR.va_lemma_aes_ctr_encrypt",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equation_Vale.AES.X64.AESCTR.aes_reqs",
"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",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_11362bdf3ed796137da93085480dc30a",
"typing_tok_Vale.AES.AES_s.AES_128@tok"
],
0,
"048f7a2137ca2650924047b2ec63cfa9"
],
[
"Vale.AES.X64.AESCTR.va_wp_aes_ctr_encrypt",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equation_Vale.AES.X64.AESCTR.aes_reqs",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"typing_tok_Vale.AES.AES_s.AES_128@tok"
],
0,
"61f331f4916385a4a1a66d0d5758f979"
],
[
"Vale.AES.X64.AESCTR.va_quick_aes_ctr_encrypt",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"f70a02947cdfb1a1ffc55a90b682d033"
],
[
"Vale.AES.X64.AESCTR.va_lemma_aes_counter_loop",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.X64.Decls.validDstAddrs128",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_e97dbe20fae743ebcc000324c0b92548",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"bb22f3e2cbbccf6b1de4fd04a87126fd"
],
[
"Vale.AES.X64.AESCTR.va_wp_aes_counter_loop",
1,
1,
0,
[
"@query", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok",
"equation_Vale.Arch.HeapImpl.vale_heap_impl",
"equation_Vale.X64.Decls.va_upd_mem",
"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",
"equation_Vale.X64.Memory.set_vale_heap",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"b9c27e538870cfd1ff27f03d2ce8d373"
],
[
"Vale.AES.X64.AESCTR.va_quick_aes_counter_loop",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"5fbecc4ba3884165173f146452a02533"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...