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.Box.fst.hints
[
"(��S�tÞ'���&z�\u0002",
[
[
"Spec.Box.publickey",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.Box.size_publickey",
"equation_Spec.Poly1305.size_key",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"39b7b33d0283977ed2e6cb8b4fb46fc3"
],
[
"Spec.Box.secretkey",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Spec.Box.size_secretkey",
"equation_Spec.Poly1305.size_key",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Poly1305.size_key"
],
0,
"c0d6fbfdff7125f74ad335b01dfa5616"
],
[
"Spec.Box.ecdh",
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.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Poly1305.size_key", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"39c69bc1f384faf8855390d71e5e9364"
],
[
"Spec.Box.box_beforenm",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"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.unsigned",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Box.ecdh",
"equation_Spec.Box.secretkey", "equation_Spec.Box.size_secretkey",
"equation_Spec.Curve25519.scalar",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"equation_Spec.Salsa20.size_nonce",
"function_token_typing_Spec.Curve25519.scalar", "int_typing",
"lemma_FStar.Pervasives.invertOption", "lemma_Lib.IntTypes.pow2_3",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some", "typing_Prims.pow2",
"typing_Spec.Box.ecdh", "typing_Spec.Poly1305.size_block",
"typing_Spec.Poly1305.size_key", "typing_Spec.Salsa20.size_nonce"
],
0,
"29dfa8001f508b873a27581aebdbb121"
],
[
"Spec.Box.box_detached_afternm",
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,
"1ccf1c7b94bf702eb5b4324d6de2bf6c"
],
[
"Spec.Box.box_detached_afternm",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"a4a963722218ab57587a6228355424f8"
],
[
"Spec.Box.box_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,
"9cf1063e52c73b8136317bf5ff3ade87"
],
[
"Spec.Box.box_detached",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Box.box_beforenm", "equation_Spec.Curve25519.scalar",
"equation_Spec.SecretBox.key", "equation_Spec.SecretBox.size_key",
"function_token_typing_Prims.int",
"function_token_typing_Spec.Curve25519.scalar",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Spec.Box.box_beforenm"
],
0,
"69049105228e007eb7e23fd14d536cc7"
],
[
"Spec.Box.box_open_detached_afternm",
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,
"a09c70c70438ac89b0b77007e70a017e"
],
[
"Spec.Box.box_open_detached_afternm",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"597219311d665e29145f1560519d021d"
],
[
"Spec.Box.box_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,
"7fa9ecf82bb2c03460908d31068a22df"
],
[
"Spec.Box.box_open_detached",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Box.box_beforenm", "equation_Spec.Curve25519.scalar",
"equation_Spec.SecretBox.key", "equation_Spec.SecretBox.size_key",
"function_token_typing_Prims.int",
"function_token_typing_Spec.Curve25519.scalar",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.Pervasives.invertOption",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Spec.Box.box_beforenm"
],
0,
"e533a0ea6d2295be5848d283aeeb0b61"
],
[
"Spec.Box.box_easy_afternm",
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,
"29bcd14f92e7989219ad1c886a25b3c2"
],
[
"Spec.Box.box_easy_afternm",
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.Salsa20.size_xnonce",
"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,
"863b82cd207bf06a358b8bb5a4787166"
],
[
"Spec.Box.box_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,
"ab82bd7c09a65b619db080b204949ff3"
],
[
"Spec.Box.box_easy",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"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.block", "equation_Spec.Poly1305.size_block",
"equation_Spec.Salsa20.size_xnonce",
"equation_Spec.SecretBox.size_tag", "equation_Spec.SecretBox.tag",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"function_token_typing_Spec.Poly1305.block",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"kinding_FStar.Pervasives.Native.tuple2@tok",
"lemma_FStar.Pervasives.invertOption",
"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",
"refinement_kinding_Tm_refine_6ea782d20d3a5b4d53411900c5408b2a"
],
0,
"52d7dcadc515333f4155c2034e67b77b"
],
[
"Spec.Box.box_open_easy_afternm",
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,
"dc8b9a79beee50bb08e4fbd9c632c071"
],
[
"Spec.Box.box_open_easy_afternm",
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,
"c5ba872a800bacd072a92ab5ca654023"
],
[
"Spec.Box.box_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,
"5b074ee6f4840b0307f2aedc3c489958"
],
[
"Spec.Box.box_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,
"87c8c161dcf13beeeb2a4ee7194a1fe9"
]
]
]
Computing file changes ...
