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
Spec.Poly1305.fst.hints
[
"��ZppA�K�?���'7a",
[
[
"Spec.Poly1305.prime",
1,
0,
0,
[ "@query" ],
0,
"e8de8b6418b4ec121bde9fa828aa04a2"
],
[
"Spec.Poly1305.fadd",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.Poly1305.felem",
"equation_Spec.Poly1305.prime", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Spec.Poly1305.prime"
],
0,
"7841b2a4f80c56b518b408a4f336dabf"
],
[
"Spec.Poly1305.fmul",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.Poly1305.felem",
"equation_Spec.Poly1305.prime", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Spec.Poly1305.prime"
],
0,
"8eb954ec6593a9caed1c6d4e0a946529"
],
[
"Spec.Poly1305.zero",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"equation_Spec.Poly1305.prime",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Spec.Poly1305.prime"
],
0,
"b1ef87b17f32343749e007639586e33a"
],
[
"Spec.Poly1305.size_block",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"73f6553ffa4ea3c5d2aeb29815c6d518"
],
[
"Spec.Poly1305.size_key",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"15f1a653524fb11ce3bcc77e89d9c877"
],
[
"Spec.Poly1305.poly1305_encode_r",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_Spec.Poly1305.size_key",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"f1248bd321db7a80c8ce9bbf3132c690"
],
[
"Spec.Poly1305.poly1305_init",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key"
],
0,
"f2f03530834557d631a387c3423c4b72"
],
[
"Spec.Poly1305.encode",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_Lib.IntTypes.SEC@tok",
"equation_Lib.ByteSequence.nat_from_bytes_le",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Poly1305.size_block", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_9a7b50ae8c4d1ef81999174593660f8c",
"refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.ByteSequence.nat_from_bytes_le",
"typing_tok_Lib.IntTypes.SEC@tok"
],
0,
"503629900454ad6afab4e1b3114f3def"
],
[
"Spec.Poly1305.poly1305_finish",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5726018248762f1a50e71a8485d6d48d",
"refinement_interpretation_Tm_refine_ca50ce86452a3257a9622c065c92c0e8",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key"
],
0,
"050dd5b4169415eff7a0acf8df52fc6b"
],
[
"Spec.Poly1305.poly1305_update_last",
1,
0,
0,
[ "@query", "equation_Spec.Poly1305.size_block" ],
0,
"d33596fe3adf0f767a4e3a718860a30f"
],
[
"Spec.Poly1305.poly1305_update",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"7069bac7114e730cb3220a45babb19c2"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...