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
Hacl.Impl.Chacha20Poly1305.PolyLemmas.fst.hints
[
"@���8\u000e�<�}.�2�$,",
[
[
"Hacl.Impl.Chacha20Poly1305.PolyLemmas.same_ctx_same_r_acc",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Hacl.Impl.Poly1305.Fields.M32",
"equality_tok_Hacl.Impl.Poly1305.Fields.M32@tok",
"equation_Hacl.Spec.Poly1305.Vec.elem",
"equation_Hacl.Spec.Poly1305.Vec.pfelem",
"equation_Hacl.Spec.Poly1305.Vec.prime",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Spec.Poly1305.felem",
"equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_key",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Spec.Poly1305.felem",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Impl.Poly1305.as_get_acc",
"typing_Hacl.Impl.Poly1305.as_get_r",
"typing_Spec.Poly1305.size_key",
"typing_tok_Hacl.Impl.Poly1305.Fields.M32@tok"
],
0,
"5f93a186bab200c25e5c9e9bf4654c98"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...