Revision 5b2fbf3c4989a9b0587a00578f69f3041df3f957 authored by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC, committed by Jonathan Protzenko on 08 April 2020, 18:59:46 UTC
1 parent d4ca892
Vale.Curve25519.Fast_lemmas_internal.fst.hints
[
"gC�\u0016H_\u001dg�P���1&�",
[
[
"Vale.Curve25519.Fast_lemmas_internal.lemma_mul_bounds_le",
1,
1,
0,
[ "@query" ],
0,
"cd08d1e183bedcb2157392d224b2071a"
],
[
"Vale.Curve25519.Fast_lemmas_internal.lemma_mul_pow2_bound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_6161103b5d8ff67ff3c6e4753e084441"
],
0,
"1afc340ec2ee7d324bdd04777b071abb"
],
[
"Vale.Curve25519.Fast_lemmas_internal.lemma_mul_pow2_bound",
2,
1,
0,
[ "@query" ],
0,
"71832c82335ed125998f5567b0aa1ca0"
],
[
"Vale.Curve25519.Fast_lemmas_internal.lemma_mul_pow2_bound",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Def.Words_s.natN",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6161103b5d8ff67ff3c6e4753e084441",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Prims.pow2"
],
0,
"72f931a56ae8ee9fd6ecd7fd55a5fd2b"
],
[
"Vale.Curve25519.Fast_lemmas_internal.lemma_mul_bound64",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"4954c3345ba5fe5f1bca2f928408de66"
],
[
"Vale.Curve25519.Fast_lemmas_internal.lemma_intel_prod_sum_bound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"f2394eee4394a279967043e48ad40aed"
],
[
"Vale.Curve25519.Fast_lemmas_internal.lemma_double_bound",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.Def.Types_s.add_wrap",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"8cfc612bbdc76e1b27942491422bcc60"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...