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.Salsa20.fst.hints
[
"��\u000f���l4�[lu�;4s",
[
[
"Spec.Salsa20.key",
1,
0,
1,
[
"@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_Prims.nat",
"equation_Spec.Salsa20.size_key", "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,
"21e20b77c9a1bb500ffbad7ae9f19298"
],
[
"Spec.Salsa20.block",
1,
0,
1,
[
"@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_Prims.nat",
"equation_Spec.Salsa20.size_block", "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,
"9bc2ee6daf27ba5e1af7cbf907413828"
],
[
"Spec.Salsa20.nonce",
1,
0,
1,
[
"@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_Prims.nat",
"equation_Spec.Salsa20.size_nonce", "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,
"b360fe8e916709a4ca33649fb5424f1f"
],
[
"Spec.Salsa20.xnonce",
1,
0,
1,
[
"@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_Prims.nat",
"equation_Spec.Salsa20.size_xnonce", "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,
"e5e6d42f77d9560c8821a1d64cdca3fe"
],
[
"Spec.Salsa20.state",
1,
0,
1,
[
"@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_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,
"b22f9937833911b7f8f56597fddcdff4"
],
[
"Spec.Salsa20.line",
1,
0,
1,
[
"@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.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.rotval", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Salsa20.idx", "equation_Spec.Salsa20.state",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0da46ef8643a6f8ea97a3358bc923338",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6f7719d2e9422e645682674727002c0b",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"46ccb44e51efddf845bb4679a1c191c3"
],
[
"Spec.Salsa20.quarter_round",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@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",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"8551fa0ebf9f34e5dc382d03d08d9e6c"
],
[
"Spec.Salsa20.column_round",
1,
0,
1,
[
"@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",
"equation_Prims.pos", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"5be1e8ce807774ee29f496e491a35216"
],
[
"Spec.Salsa20.row_round",
1,
0,
1,
[
"@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",
"equation_Prims.pos", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"5e8617c42c73b7791a0e6b185b7953c3"
],
[
"Spec.Salsa20.salsa20_add_counter",
1,
0,
1,
[
"@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.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.Salsa20.counter",
"int_inversion", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"acc790efe66abd70aa2ea424966b1ea1"
],
[
"Spec.Salsa20.salsa20_core",
1,
0,
1,
[
"@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_Prims.nat",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"39b2468dc0f7804ef9b56a92b2a3fb4f"
],
[
"Spec.Salsa20.constant0",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "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,
"92bb95c4fd891b4d26363b182c3bf59c"
],
[
"Spec.Salsa20.constant1",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "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,
"a7c86850a410a7c3f452a1bcee13440b"
],
[
"Spec.Salsa20.constant2",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "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,
"036c0a9ef197243bdf98a1d35aa14e9a"
],
[
"Spec.Salsa20.constant3",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "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,
"6366a6566525fe992e1105a8787f3698"
],
[
"Spec.Salsa20.setup",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.counter",
"equation_Spec.Salsa20.key", "equation_Spec.Salsa20.size_key",
"equation_Spec.Salsa20.state",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_003235b3c3b0fd738352c1e62cb8eccd",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_17eb0b9d8c560b31f7749972be12ed74",
"refinement_interpretation_Tm_refine_1c31ca88fe307e934f4c6728801e3754",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_44e5fc474a070a18a3b076585da92fd5",
"refinement_interpretation_Tm_refine_4a0d4304a3a1dfdb80a3b3dddc3e3f20",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_719ff7b2ff98fd64eace28b528e77052",
"refinement_interpretation_Tm_refine_7d4ad4ab76779619b6b2cf8d5c76be32",
"refinement_interpretation_Tm_refine_81acc738f3b19503bc01e0bca5ddde4b",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a400615de3176203e22fa9eb08adf556",
"refinement_interpretation_Tm_refine_a53090a6ae7c0a8bb507d8bfb56d7bdd",
"refinement_interpretation_Tm_refine_adb54abff4a0780ca27ab9cfe1ec6776",
"refinement_interpretation_Tm_refine_cf54dad6a0e83543dc7b88660bc3e4e5",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.v",
"typing_Spec.Salsa20.constant0", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"a75e92a45b5b3f250738fd485b450067"
],
[
"Spec.Salsa20.salsa20_init",
1,
0,
1,
[
"@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.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Spec.Salsa20.key",
"equation_Spec.Salsa20.size_key",
"function_token_typing_Lib.IntTypes.uint8",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length"
],
0,
"c810b46657e8c733d8a04fcbe6813a39"
],
[
"Spec.Salsa20.xsetup",
1,
0,
1,
[
"@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",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Salsa20.key",
"equation_Spec.Salsa20.size_key", "equation_Spec.Salsa20.state",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"lemma_FStar.UInt.pow2_values", "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_17eb0b9d8c560b31f7749972be12ed74",
"refinement_interpretation_Tm_refine_1c31ca88fe307e934f4c6728801e3754",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4a0d4304a3a1dfdb80a3b3dddc3e3f20",
"refinement_interpretation_Tm_refine_81acc738f3b19503bc01e0bca5ddde4b",
"refinement_interpretation_Tm_refine_b8165395463969fbe87a6448c1f75b07",
"refinement_interpretation_Tm_refine_bc23993b76acb07c71baac3d1798b4fa",
"refinement_interpretation_Tm_refine_c740246281d0ffa10a1422d129fa0039",
"refinement_interpretation_Tm_refine_cf54dad6a0e83543dc7b88660bc3e4e5",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_e73fcff5e930b7b6b76169f43fa943b1",
"typing_FStar.Seq.Base.length"
],
0,
"cb909b524d25af66be7daf5c0cf2a525"
],
[
"Spec.Salsa20.hsalsa20_init",
1,
0,
1,
[
"@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.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Spec.Salsa20.key",
"equation_Spec.Salsa20.size_key",
"function_token_typing_Lib.IntTypes.uint8",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length"
],
0,
"5450bc382045d08088b73f12aaf2e847"
],
[
"Spec.Salsa20.hsalsa20",
1,
0,
1,
[
"@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.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.key",
"equation_Spec.Salsa20.size_key",
"function_token_typing_Lib.IntTypes.uint8",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a0af5ec1cd802f74642c75324f1476af",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.v",
"typing_Spec.Salsa20.constant2", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"1d242d62788f9e8d976bb1300c95320b"
],
[
"Spec.Salsa20.salsa20_key_block",
1,
0,
1,
[
"@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.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Prims.pos", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"b1fb32265cda503f0844138eff41936c"
],
[
"Spec.Salsa20.salsa20_key_block0",
1,
0,
1,
[
"@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.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.pos", "equation_Spec.Salsa20.key",
"equation_Spec.Salsa20.size_key",
"function_token_typing_Lib.IntTypes.uint8",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length", "typing_Prims.pow2"
],
0,
"76904c7174c427271e6343dccdd7e592"
],
[
"Spec.Salsa20.xor_block",
1,
0,
1,
[
"@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",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"4d5ba30d4536de67953f2f21af148e9b"
],
[
"Spec.Salsa20.salsa20_encrypt_last",
1,
0,
1,
[
"@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.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_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.Salsa20.size_block",
"equation_Spec.Salsa20.size_nonce", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_3",
"primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_03ee14973b2317c1424ffe90b7429d07",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_9422d419556855bb96a4044bcf637786",
"refinement_interpretation_Tm_refine_a2edd2054ec8619a5dc566d75e1a5f28",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_Spec.Salsa20.size_nonce", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"9f3e256d2b37bb465a8ee00b86e6dde3"
],
[
"Spec.Salsa20.salsa20_update",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.Salsa20.size_block",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"416d1307adbd2e7ca56ae9a3bf3bbe31"
],
[
"Spec.Salsa20.salsa20_update",
2,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.Salsa20.size_block",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"ce9c39d92c8b48797b5f07e228104330"
],
[
"Spec.Salsa20.salsa20_update",
3,
0,
1,
[
"@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.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.Salsa20.size_block", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6ed871b7343aeb6d991fec480e67cf62",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"e34531389d3fed5dbb947d073c4a0f89"
],
[
"Spec.Salsa20.salsa20_encrypt_bytes",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.Salsa20.size_block",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"e802a0328ccb8104f69c84588e1a6534"
],
[
"Spec.Salsa20.salsa20_encrypt_bytes",
2,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.Salsa20.size_block",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"21a7e1ea7d05fced7833c12073712f07"
],
[
"Spec.Salsa20.salsa20_decrypt_bytes",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.Salsa20.size_block",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"5555b9e84c88042803e55b7a6d668418"
],
[
"Spec.Salsa20.salsa20_decrypt_bytes",
2,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.Salsa20.size_block",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0"
],
0,
"a2aa41a9f6b235aac610e6febfd1d4be"
],
[
"Spec.Salsa20.salsa20_decrypt_bytes",
3,
0,
1,
[ "@query" ],
0,
"d529fcffce5ce9b8acd89eed5b929606"
]
]
]
Computing file changes ...
