[
  "'┘z§'┴ĻÆ┼Ét8D³ø7",
  [
    [
      "Spec.Salsa20.key",
      1,
      0,
      1,
      [
        "@query", "equation_Spec.Salsa20.keylen",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Spec.Salsa20.block",
      1,
      0,
      1,
      [
        "@query", "equation_Spec.Salsa20.blocklen",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Spec.Salsa20.nonce",
      1,
      0,
      1,
      [
        "@query", "equation_Spec.Salsa20.noncelen",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Spec.Salsa20.counter",
      1,
      0,
      1,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0
    ],
    [
      "Spec.Salsa20.state",
      1,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Spec.Salsa20.line",
      1,
      0,
      1,
      [
        "@query", "equation_FStar.UInt32.t", "equation_Prims.nat",
        "equation_Spec.Salsa20.idx", "equation_Spec.Salsa20.state",
        "int_inversion", "kinding_FStar.UInt32.t_@tok",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "refinement_interpretation_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0
    ],
    [
      "Spec.Salsa20.quarter_round",
      1,
      0,
      1,
      [
        "@query", "b2t_def", "bool_inversion", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt32.n",
        "equation_Prims.nat", "function_token_typing_FStar.UInt32.n",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.UInt.fits"
      ],
      0
    ],
    [
      "Spec.Salsa20.column_round",
      1,
      0,
      1,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0
    ],
    [
      "Spec.Salsa20.row_round",
      1,
      0,
      1,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0
    ],
    [
      "Spec.Salsa20.rounds",
      1,
      0,
      1,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0
    ],
    [
      "Spec.Salsa20.salsa20_core",
      1,
      0,
      1,
      [
        "@query", "equation_FStar.UInt32.t", "equation_Prims.nat",
        "equation_Spec.Salsa20.shuffle", "equation_Spec.Salsa20.state",
        "fuel_correspondence_Spec.Salsa20.rounds.fuel_instrumented",
        "function_token_typing_Spec.Salsa20.rounds",
        "interpretation_Tm_arrow_f82c3fb9ac6610efb97620a59b378092",
        "refinement_interpretation_Tm_refine_549582658154778e4c9eff5e5f77503c",
        "refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b"
      ],
      0
    ],
    [
      "Spec.Salsa20.constant0",
      1,
      0,
      1,
      [
        "@query", "b2t_def", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt32.n",
        "equation_Prims.nat", "function_token_typing_FStar.UInt32.n",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0
    ],
    [
      "Spec.Salsa20.constant1",
      1,
      0,
      1,
      [
        "@query", "b2t_def", "data_elim_FStar.UInt32.Mk",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
        "equation_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant0",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d"
      ],
      0
    ],
    [
      "Spec.Salsa20.constant2",
      1,
      0,
      1,
      [
        "@query", "b2t_def", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt32.n",
        "equation_Prims.nat", "function_token_typing_FStar.UInt32.n",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0
    ],
    [
      "Spec.Salsa20.constant3",
      1,
      0,
      1,
      [
        "@query", "b2t_def", "data_elim_FStar.UInt32.Mk",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
        "equation_Spec.Salsa20.constant2",
        "function_token_typing_Spec.Salsa20.constant2",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d"
      ],
      0
    ],
    [
      "Spec.Salsa20.setup",
      1,
      0,
      1,
      [
        "@query", "b2t_def", "data_elim_FStar.UInt32.Mk",
        "equation_FStar.Mul.op_Star", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt32.t",
        "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt8.t",
        "equation_Prims.nat", "equation_Spec.Lib.lbytes",
        "equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.counter",
        "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen",
        "function_token_typing_Spec.Salsa20.constant2", "int_inversion",
        "kinding_FStar.UInt8.t_@tok", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_49c726ebbffbe257a62940bb9bbe9619",
        "refinement_interpretation_Tm_refine_54c03c78d7539eae7ee3b6a012705328",
        "refinement_interpretation_Tm_refine_a38ba213f7d10ad82997d9720a14fea1",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "typing_FStar.Seq.Base.length"
      ],
      0
    ],
    [
      "Spec.Salsa20.setup",
      2,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Spec.Salsa20.salsa20_block",
      1,
      0,
      1,
      [
        "@query", "equation_FStar.Int16.n", "equation_FStar.Mul.op_Star",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.t",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.counter",
        "equation_Spec.Salsa20.salsa20_core", "equation_Spec.Salsa20.state",
        "function_token_typing_FStar.Int16.n", "int_inversion", "int_typing",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
        "typing_FStar.Mul.op_Star", "typing_Spec.Salsa20.salsa20_core",
        "typing_Spec.Salsa20.setup"
      ],
      0
    ],
    [
      "Spec.Salsa20.salsa20_ctx",
      1,
      0,
      1,
      [
        "@query", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Spec.Salsa20.salsa20_cipher",
      1,
      0,
      1,
      [
        "@query", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen"
      ],
      0
    ],
    [
      "Spec.Salsa20.salsa20_encrypt_bytes",
      1,
      0,
      1,
      [
        "@query", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen"
      ],
      0
    ]
  ]
]