[
  "�'.�\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,
      "7262929bd614806002ddd27e4f53a817"
    ],
    [
      "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,
      "602ad7ee64afe1ef30e9eb92829da567"
    ],
    [
      "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,
      "5a4fb7dc00ba6fe79c451fa4d9fc9f9a"
    ],
    [
      "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,
      "a23e3bac7708f708979537d674d2879a"
    ],
    [
      "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,
      "633ef0e7d8576446ab008741622ffbaa"
    ],
    [
      "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,
      "3a407a36b53ec0793c960d9397cbd4c5"
    ],
    [
      "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,
      "35260c17c237831f6950805eb1845372"
    ],
    [
      "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,
      "f03b44f583008a026557ea5dbc7cfab2"
    ],
    [
      "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,
      "347d036955533e217896fd7b0c019ec5"
    ]
  ]
]