Revision e56414221fb67ecff7d071497f8ba5d20e9c5ba9 authored by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC, committed by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC
1 parent db297bf
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,
"c5a409f1666e941c263e727b5cd47b30"
],
[
"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,
"3f4db3d6fc235d7194adca8da1bee27c"
],
[
"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,
"20046317efe2c66310f250193b91229c"
],
[
"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,
"aa3e0339d7edf3aa010248acf5ba26e8"
],
[
"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,
"50754329f84f1f3efb93e78befd45a15"
],
[
"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,
"0495b0ecace2440defb8f52ab488dbe2"
],
[
"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,
"dd78b66456f33f74f784dd420f51442c"
],
[
"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,
"9eaf297baf597978b86cc391eddaa26f"
],
[
"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,
"bc5962a92b5bedaa67eb22931f209c90"
],
[
"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,
"bd99a315f9fceab8250563cf608e06f5"
]
]
]
Computing file changes ...
