Revision c596c6bb21e6e478e0b46159ef182ccce6a695cb authored by Konrad Kohbrok on 16 April 2018, 13:51:58 UTC, committed by Konrad Kohbrok on 16 April 2018, 13:51:58 UTC
1 parent 68d3953
Spec.Poly1305.Lemmas.fst.hints
[
"1Hic��\u007f\\�U9��u�i",
[
[
"Spec.Poly1305.Lemmas.lemma_prime_value",
1,
2,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.Poly1305.Lemmas.lemma_prime_value",
2,
2,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.Poly1305.Lemmas.lemma_prime_value",
3,
2,
1,
[
"@query", "equation_Prims.nat",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Spec.Poly1305.Lemmas.lemma_prime_value",
4,
2,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.Poly1305.Lemmas.lemma_encode_bound",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_FStar.Mul.op_Star", "equation_FStar.UInt32.n",
"equation_FStar.UInt8.t", "equation_Prims.nat",
"function_token_typing_FStar.UInt32.n", "kinding_FStar.UInt8.t_@tok",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.Poly1305.Lemmas_Tm_refine_2c4751014d16f1ec8b1f34b6cc3b2faa",
"typing_FStar.Seq.Base.length"
],
0
],
[
"Spec.Poly1305.Lemmas.lemma_encode_bound",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_FStar.Mul.op_Star", "equation_FStar.UInt32.n",
"equation_FStar.UInt8.t", "equation_Prims.nat",
"function_token_typing_FStar.UInt32.n", "kinding_FStar.UInt8.t_@tok",
"lemma_Spec.Poly1305.Lemmas.lemma_prime_value",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.Poly1305.Lemmas_Tm_refine_2c4751014d16f1ec8b1f34b6cc3b2faa",
"typing_FStar.Seq.Base.length"
],
0
],
[
"Spec.Poly1305.Lemmas.lemma_encode_r",
1,
2,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.Poly1305.Lemmas.lemma_encode_r",
2,
2,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.Poly1305.Lemmas.lemma_encode_r",
3,
2,
1,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0
],
[
"Spec.Poly1305.Lemmas.lemma_encode_r",
4,
2,
1,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0
],
[
"Spec.Poly1305.Lemmas.lemma_encode_r",
5,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Mul.op_Star",
"equation_FStar.UInt8.t", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Spec.Poly1305.Lemmas_Tm_refine_aca10fb50cc7162d8b55c168416f714b"
],
0
],
[
"Spec.Poly1305.Lemmas.lemma_encode_r",
6,
2,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
]
]
]
Computing file changes ...