Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Hacl.Spec.Poly1305.Vec.fst.hints
[
"�\u0011el\u0005v��\r\u00003�B�)G",
[
[
"Hacl.Spec.Poly1305.Vec.lemma_pow2_128",
1,
0,
0,
[ "@query" ],
0,
"6e35bbfb454f3b53838c3f7c8459b175"
],
[
"Hacl.Spec.Poly1305.Vec.from_elem",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.width", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "int_inversion",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"2e943bc037c60fc2631687d92051bf6d"
],
[
"Hacl.Spec.Poly1305.Vec.zero",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"equation_Spec.Poly1305.prime",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Spec.Poly1305.prime"
],
0,
"a76942c9e81116fdf2eacd71f9fa3389"
],
[
"Hacl.Spec.Poly1305.Vec.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",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"a86511c58d3c8600cea1c3ea072a7d43"
],
[
"Hacl.Spec.Poly1305.Vec.load_elem1",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.block", "equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "int_typing",
"lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128",
"primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Spec.Poly1305.size_key"
],
0,
"c370160a5912dd973e871df6828bec3f"
],
[
"Hacl.Spec.Poly1305.Vec.load_elem2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"7748faa15d1158f48211dd82ca66fc4f"
],
[
"Hacl.Spec.Poly1305.Vec.load_elem2",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "int_typing",
"lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_38d381fc275b9c5d3a568336a73accd5",
"refinement_interpretation_Tm_refine_3b1c0c65bc4d6bcc32d56edbecd6f8c1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_eed93d731370f7c1b5b21d0db49acad9",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key"
],
0,
"47f11e8e0f4dc276e3cb92bdc8a252ae"
],
[
"Hacl.Spec.Poly1305.Vec.load_elem4",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key"
],
0,
"dc825aeaab1d1a2feb5c38080545d581"
],
[
"Hacl.Spec.Poly1305.Vec.load_elem4",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "int_typing",
"lemma_FStar.UInt.pow2_values",
"lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_39c242f89c59a5dcdff340e1c7b106e9",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_63549f5366714a9880f518a73445f045",
"refinement_interpretation_Tm_refine_7165b76f0afec12e4fc5e3e5a352bbb6",
"refinement_interpretation_Tm_refine_7498945fa63395a72eda90b148a76b40",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.v", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"a5254093014be6b2131a993b9c32062f"
],
[
"Hacl.Spec.Poly1305.Vec.load_elem",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key"
],
0,
"4d731b15b3186491dd2592c2d8c3bdd3"
],
[
"Hacl.Spec.Poly1305.Vec.load_elem",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Lib.Sequence.lseq", "equation_Spec.Poly1305.size_block",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"7ca9b4ca53da3d08a03dfcf67f122532"
],
[
"Hacl.Spec.Poly1305.Vec.load_blocks",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key"
],
0,
"e14e5a00ca66d54b8369a3f16fd0adb7"
],
[
"Hacl.Spec.Poly1305.Vec.load_blocks",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"equation_Lib.IntVector.width", "equation_Prims.nat", "int_typing",
"lemma_Hacl.Spec.Poly1305.Vec.lemma_pow2_128",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181"
],
0,
"cfb4dfb5f16c345eb57309364442c715"
],
[
"Hacl.Spec.Poly1305.Vec.load_acc1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.Poly1305.size_key",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"16f9541fcb632a00982fe66957cb18f7"
],
[
"Hacl.Spec.Poly1305.Vec.load_acc2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"752e03eb763fc831fa3a891d6e81bbeb"
],
[
"Hacl.Spec.Poly1305.Vec.load_acc2",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
"equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_key",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
"typing_Spec.Poly1305.size_key"
],
0,
"3b126708054dd6be38f91c865db3db6f"
],
[
"Hacl.Spec.Poly1305.Vec.load_acc4",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key"
],
0,
"75973636baecb6ece67ccc840dfb17b6"
],
[
"Hacl.Spec.Poly1305.Vec.load_acc4",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Poly1305.Vec.pfelem", "equation_Prims.nat",
"equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_key",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
"typing_Spec.Poly1305.size_key"
],
0,
"76c49dc15dcb78dbd98b275b320c9785"
],
[
"Hacl.Spec.Poly1305.Vec.load_acc",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key"
],
0,
"0f33ac0a1a281ce877fc25d25cb0a2f6"
],
[
"Hacl.Spec.Poly1305.Vec.load_acc",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Lib.Sequence.lseq", "equation_Spec.Poly1305.size_block",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"cae446dc167efd8ee5eb2367282e5823"
],
[
"Hacl.Spec.Poly1305.Vec.normalize_1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Spec.Poly1305.size_block",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_block"
],
0,
"af52150bce685c8364ab3739dbe91dc3"
],
[
"Hacl.Spec.Poly1305.Vec.normalize_1",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key"
],
0,
"768246a60dc7d00b5273e7a680df65aa"
],
[
"Hacl.Spec.Poly1305.Vec.normalize_2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Spec.Poly1305.size_block",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_block"
],
0,
"a4fcbb13f2b6374107e1cbe7aae312b3"
],
[
"Hacl.Spec.Poly1305.Vec.normalize_2",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.Poly1305.size_key",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"141022398528b289a4e81090733a33f7"
],
[
"Hacl.Spec.Poly1305.Vec.normalize_4",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Spec.Poly1305.size_block",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_block"
],
0,
"23b886cf9b8578eaba39d5909644482b"
],
[
"Hacl.Spec.Poly1305.Vec.normalize_4",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.Poly1305.size_key",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"22440ee8b5938ebaab52f28ab563ea29"
],
[
"Hacl.Spec.Poly1305.Vec.normalize_n",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Poly1305.Vec.elem",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"equation_Hacl.Spec.Poly1305.Vec.pfelem",
"equation_Lib.Sequence.lseq",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"1dd820f38b455f7641e8a4d25743ac9a"
],
[
"Hacl.Spec.Poly1305.Vec.compute_r1",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.Poly1305.size_key",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"c841eda18b7a25fb028df499085aa3db"
],
[
"Hacl.Spec.Poly1305.Vec.compute_r2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.Poly1305.size_key",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"f133e4eb8f587f69f2fa0d71adf7d626"
],
[
"Hacl.Spec.Poly1305.Vec.compute_r4",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.Poly1305.size_key",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"56baf68c28a39ed6b34f48226c876729"
],
[
"Hacl.Spec.Poly1305.Vec.compute_rw",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181"
],
0,
"9951e799f69aeb9e024b92cca49fd16f"
],
[
"Hacl.Spec.Poly1305.Vec.poly1305_update_nblocks",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key"
],
0,
"5990f8603243de874ff00e32f389c302"
],
[
"Hacl.Spec.Poly1305.Vec.poly1305_update_multi",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block",
"primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"a535fe25c416eea00beb7c3b1d97646a"
],
[
"Hacl.Spec.Poly1305.Vec.poly1305_update_multi",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Spec.AES.elem", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_09630c7d170f75d893f43322b29ffb46",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_22f14c48c4531dc45e8e4259f8a1add4",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.Sequence.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key"
],
0,
"33a256df47d80f15f84dc56f0fcdace1"
],
[
"Hacl.Spec.Poly1305.Vec.poly1305_update_vec",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"equation_Hacl.Spec.Poly1305.Vec.pfelem",
"equation_Hacl.Spec.Poly1305.Vec.size_block",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.width", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.felem",
"equation_Spec.Poly1305.size_block",
"function_token_typing_Spec.AES.elem", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Division", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.minint", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"7cf45f73ddcf108b6fb9871ec89946e9"
],
[
"Hacl.Spec.Poly1305.Vec.poly1305_update",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Poly1305.Vec.lanes",
"equation_Spec.Poly1305.size_key",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_a658c976a9118ef6c4559f187aff2181",
"typing_Spec.Poly1305.size_key"
],
0,
"3dedea751a7ceb168b37cc58a6a4f114"
]
]
]
Computing file changes ...
