Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
Hacl.Curve25519.Finv.Field51.fst.hints
[
"\u0001g�\u0003\u0010���L��d�=�",
[
[
"Hacl.Curve25519.Finv.Field51.fsquare_times_51",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947"
],
0,
"94da9c6ced6320ee9c5876ff42b99bff"
],
[
"Hacl.Curve25519.Finv.Field51.finv_51",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.nat", "equation_Spec.Curve25519.prime", "int_typing",
"lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"95ebd998b4a8ded4148f25e5eff6607a"
],
[
"Hacl.Curve25519.Finv.Field51.finv_51",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M51",
"equality_tok_Hacl.Impl.Curve25519.Fields.Core.M51@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Hacl.Impl.Curve25519.Fields.Core.felem",
"equation_Hacl.Impl.Curve25519.Fields.Core.felem_wide2",
"equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.IntTypes.uint128", "equation_Lib.IntTypes.uint64",
"function_token_typing_Lib.IntTypes.uint128",
"function_token_typing_Lib.IntTypes.uint64",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"refinement_interpretation_Tm_refine_5064087b76eb6f995808483f3366af91",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_e4ea1e84380edcecf7c70a639d08b578",
"typing_Lib.Buffer.loc", "typing_tok_Lib.Buffer.MUT@tok"
],
0,
"dd108570b9894723124b626da25a0781"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...