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
Spec.SecretBox.fst.hints
[
"�'.�\u00106-tN��,�V��",
[
[
"Spec.SecretBox.key",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.Poly1305.size_key",
"equation_Spec.SecretBox.size_key",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"f46b0691e1f3efbc3b2571087faa45a4"
],
[
"Spec.SecretBox.aekey",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Spec.Poly1305.size_key",
"equation_Spec.SecretBox.size_key", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"84016c955cb626aae9ec63fd3f0f1d61"
],
[
"Spec.SecretBox.nonce",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.Poly1305.size_key",
"equation_Spec.SecretBox.size_nonce",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"b915501479361ec245e76e854dee16bc"
],
[
"Spec.SecretBox.tag",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.Poly1305.size_key",
"equation_Spec.SecretBox.size_tag",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"658a1e31516fb0d0a9892947489ac44b"
],
[
"Spec.SecretBox.secretbox_init",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "equation_Spec.Salsa20.constant2",
"equation_Spec.SecretBox.size_nonce",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a0af5ec1cd802f74642c75324f1476af",
"typing_Lib.IntTypes.v", "typing_Spec.Poly1305.size_block",
"typing_Spec.Poly1305.size_key", "typing_Spec.Salsa20.constant2",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"90eef8418c97ebae5e49836334fd495b"
],
[
"Spec.SecretBox.get_len0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.Poly1305.size_key", "int_inversion",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Spec.Poly1305.size_key"
],
0,
"48b3f18ee0c88d9cf2a8585f36646e4b"
],
[
"Spec.SecretBox.secretbox_detached",
1,
0,
0,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.SecretBox.size_block",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"fa532d038ae8a6db8016a5ba44ca3942"
],
[
"Spec.SecretBox.secretbox_detached",
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.U32@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.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "equation_Spec.Salsa20.constant2",
"equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.size_block",
"equation_Spec.Salsa20.size_nonce", "equation_Spec.SecretBox.aekey",
"equation_Spec.SecretBox.get_len0", "equation_Spec.SecretBox.key",
"equation_Spec.SecretBox.nonce",
"equation_Spec.SecretBox.secretbox_init",
"equation_Spec.SecretBox.size_block",
"equation_Spec.SecretBox.size_key",
"equation_Spec.SecretBox.size_nonce",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_1e2f63b7b52e41f2219854b123bca09c",
"refinement_interpretation_Tm_refine_26d768cc241c6628db9e0d45d45d9136",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_484ce31289f472b3c103679b06f9e35f",
"refinement_interpretation_Tm_refine_4fbf60df9e1427f1128eefb59f582a34",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5a1574f241a77e0dfe3e6ffe15df50fa",
"refinement_interpretation_Tm_refine_6301f4fab42605ee7b26ae67177dd341",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_86b5adc835b032412d8661e32f0b7695",
"refinement_interpretation_Tm_refine_9c2c4d03687365eff8fcbb4e2dca047a",
"refinement_interpretation_Tm_refine_a0af5ec1cd802f74642c75324f1476af",
"refinement_interpretation_Tm_refine_b4df1d1f2ad218928d5d997e265c58d6",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
"refinement_interpretation_Tm_refine_f1a872fcdff01fb7176b4471b0bf3cb1",
"refinement_interpretation_Tm_refine_f72e84af70b24071997928fe8b6519f9",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.v", "typing_Lib.Sequence.length",
"typing_Prims.pow2", "typing_Spec.Poly1305.size_block",
"typing_Spec.Poly1305.size_key", "typing_Spec.Salsa20.constant2",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"73948a8978b0f393c607c816f1b437f6"
],
[
"Spec.SecretBox.secretbox_open_detached",
1,
0,
0,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.SecretBox.size_block",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"cf1d343232693b0ddd0611c6355a5a21"
],
[
"Spec.SecretBox.secretbox_open_detached",
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.U32@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.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "equation_Spec.Poly1305.to_felem",
"equation_Spec.Poly1305.zero", "equation_Spec.Salsa20.constant2",
"equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.size_block",
"equation_Spec.Salsa20.size_nonce", "equation_Spec.SecretBox.aekey",
"equation_Spec.SecretBox.get_len0", "equation_Spec.SecretBox.key",
"equation_Spec.SecretBox.nonce",
"equation_Spec.SecretBox.secretbox_init",
"equation_Spec.SecretBox.size_block",
"equation_Spec.SecretBox.size_key",
"equation_Spec.SecretBox.size_nonce",
"equation_Spec.SecretBox.size_tag",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_1e2f63b7b52e41f2219854b123bca09c",
"refinement_interpretation_Tm_refine_26d768cc241c6628db9e0d45d45d9136",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_484ce31289f472b3c103679b06f9e35f",
"refinement_interpretation_Tm_refine_4fbf60df9e1427f1128eefb59f582a34",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5a1574f241a77e0dfe3e6ffe15df50fa",
"refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_86b5adc835b032412d8661e32f0b7695",
"refinement_interpretation_Tm_refine_887a0fa1b773a9238a9c5628865350af",
"refinement_interpretation_Tm_refine_9c2c4d03687365eff8fcbb4e2dca047a",
"refinement_interpretation_Tm_refine_a0af5ec1cd802f74642c75324f1476af",
"refinement_interpretation_Tm_refine_b4df1d1f2ad218928d5d997e265c58d6",
"refinement_interpretation_Tm_refine_c8961f5ea186e52375394e443e33dbc9",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
"refinement_interpretation_Tm_refine_f1a872fcdff01fb7176b4471b0bf3cb1",
"refinement_interpretation_Tm_refine_f72e84af70b24071997928fe8b6519f9",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.v",
"typing_Lib.Sequence.length", "typing_Prims.pow2",
"typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key",
"typing_Spec.Poly1305.zero", "typing_Spec.Salsa20.constant2",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"9d4ea67dd0aa098690c7bbfc5ee89d84"
],
[
"Spec.SecretBox.secretbox_easy",
1,
0,
0,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.SecretBox.size_block",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"edb262a10f17a276734111744e328f7b"
],
[
"Spec.SecretBox.secretbox_easy",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Poly1305.size_block",
"equation_Spec.SecretBox.size_tag", "equation_Spec.SecretBox.tag",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Seq.Base.lemma_len_append",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_6ea782d20d3a5b4d53411900c5408b2a",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"fb1353b5a70f7f9d281ed563979e2e1c"
],
[
"Spec.SecretBox.secretbox_open_easy",
1,
0,
0,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.SecretBox.size_block",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"fe6b0e0a0edf2e7aa70ada2eb1976324"
],
[
"Spec.SecretBox.secretbox_open_easy",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Spec.Poly1305.size_block",
"equation_Spec.SecretBox.size_tag",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2e2eaf1583653b9f5c3d2bde77407586",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_Lib.Sequence.length", "typing_Spec.Poly1305.size_block"
],
0,
"d3304d5f547c1627fbbb9f2215c8995b"
]
]
]
Computing file changes ...
