Revision 059787e63538941130606248805cab290fdbc5d7 authored by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC, committed by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC
1 parent 03f1e46
Vale.AES.X64.GHash.fsti.hints
[
"���.�����\u001bU��Z�",
[
[
"Vale.AES.X64.GHash.get_last_slice_workaround",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_AmpAmp",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647"
],
0,
"75c15195c3a1afc417fdfb7436173be0"
],
[
"Vale.AES.X64.GHash.va_quick_Compute_ghash_incremental_register",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
],
0,
"be4a48cb08f9592b70a35f2419b549b7"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...