[
  "\u0002ž<L—ýb»ž†¬-/šLJ",
  [
    [
      "Hacl.Impl.Salsa20.state",
      1,
      2,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.op_Less_Less_Less",
      1,
      2,
      1,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing",
        "data_elim_FStar.UInt32.Mk", "data_elim_Spec.CTR.Mkblock_cipher_ctx",
        "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.UInt32.v", "equation_Hacl.Impl.Salsa20.u32",
        "equation_Prims.nat", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant2",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "function_token_typing_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant2",
        "function_token_typing_Spec.Salsa20.salsa20_ctx",
        "lemma_FStar.Buffer.lemma_size", "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_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_9941a4ed3911ef331a8db7c7fbf2373b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.UInt32.v"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.setup",
      1,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.setup",
      2,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.setup",
      3,
      0,
      1,
      [
        "@query", "equation_FStar.UInt32.t", "equation_FStar.UInt8.t",
        "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt32.t",
        "equation_Hacl.UInt8.t", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "refinement_interpretation_Tm_refine_173c3f7fb931ea8e37f2cd554b93e659",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_d0248a37b555c45264d4be3b1e2a8bff"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.setup",
      4,
      0,
      0,
      [
        "@query", "assumption_FStar.HyperHeap.HasEq_rid", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.contains", "equation_FStar.Buffer.content",
        "equation_FStar.Buffer.disjoint", "equation_FStar.Buffer.equal",
        "equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.idx",
        "equation_FStar.Buffer.includes", "equation_FStar.Buffer.length",
        "equation_FStar.Buffer.live", "equation_FStar.Buffer.sub",
        "equation_FStar.HyperHeap.map_invariant",
        "equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.contains",
        "equation_FStar.HyperStack.equal_domains",
        "equation_FStar.HyperStack.frameOf",
        "equation_FStar.HyperStack.fresh_frame",
        "equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_in",
        "equation_FStar.HyperStack.is_tip",
        "equation_FStar.HyperStack.live_region",
        "equation_FStar.HyperStack.pop",
        "equation_FStar.HyperStack.poppable", "equation_FStar.Mul.op_Star",
        "equation_FStar.ST.inline_stack_inv", "equation_FStar.Set.eqtype",
        "equation_FStar.UInt.add", "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.add", "equation_FStar.UInt32.n",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
        "equation_FStar.UInt32.v", "equation_FStar.UInt64.t",
        "equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v",
        "equation_FStar.UInt8.t", "equation_Hacl.Cast.uint32_to_sint32",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.Lib.Create.h32",
        "equation_Hacl.UInt32.t", "equation_Hacl.UInt8.t",
        "equation_Prims.nat", "equation_Spec.Salsa20.constant0",
        "equation_Spec.Salsa20.constant1", "equation_Spec.Salsa20.constant2",
        "equation_Spec.Salsa20.constant3", "equation_Spec.Salsa20.setup",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_guarded_inversion_FStar.HyperStack.reference",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "fuel_guarded_inversion_FStar.UInt64.t_",
        "function_token_typing_FStar.Heap.emp",
        "function_token_typing_FStar.Heap.heap",
        "function_token_typing_FStar.HyperHeap.rid", "int_typing",
        "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok",
        "lemma_FStar.Buffer.lemma_disjoint_symm",
        "lemma_FStar.Buffer.lemma_equal_domains_2",
        "lemma_FStar.Buffer.lemma_fresh_poppable",
        "lemma_FStar.Buffer.lemma_live_disjoint",
        "lemma_FStar.Buffer.lemma_modifies_0_1",
        "lemma_FStar.Buffer.lemma_modifies_0_1_",
        "lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped",
        "lemma_FStar.Buffer.modifies_poppable_1",
        "lemma_FStar.Buffer.modifies_popped_1",
        "lemma_FStar.Buffer.modifies_subbuffer_1",
        "lemma_FStar.Buffer.no_upd_fresh",
        "lemma_FStar.Buffer.no_upd_lemma_0",
        "lemma_FStar.Buffer.no_upd_lemma_1",
        "lemma_FStar.Buffer.no_upd_popped",
        "lemma_FStar.HyperStack.lemma_equal_domains_trans",
        "pretyping_6c86c071b92797cdf01eb016249a9465",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "proj_equation_FStar.Buffer.MkBuffer_idx",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.Buffer.MkBuffer_max_length",
        "proj_equation_FStar.HyperStack.HS_h",
        "proj_equation_FStar.HyperStack.MkRef_id",
        "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Buffer.MkBuffer_idx",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_0dc1829dbc3c1d1c42b7a4e9e5c89884",
        "refinement_interpretation_Tm_refine_173c3f7fb931ea8e37f2cd554b93e659",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d0248a37b555c45264d4be3b1e2a8bff",
        "refinement_interpretation_Tm_refine_de8123dd3e45084cdea7d9d0e7ffb100",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Tm_refine_f59487b7e8b45c2a070787f5739c33a0",
        "refinement_interpretation_Tm_refine_f7e852e409990c1c56f7fc4e17e0851b",
        "refinement_kinding_Tm_refine_a121f8bda6f05793d62ed0cfe5b942df",
        "typing_FStar.Buffer.__proj__MkBuffer__item__content",
        "typing_FStar.Buffer.__proj__MkBuffer__item__idx",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.Buffer.__proj__MkBuffer__item__max_length",
        "typing_FStar.Buffer.content", "typing_FStar.Buffer.idx",
        "typing_FStar.Buffer.length", "typing_FStar.HyperHeap.includes",
        "typing_FStar.HyperStack.__proj__HS__item__h",
        "typing_FStar.HyperStack.__proj__HS__item__tip",
        "typing_FStar.HyperStack.__proj__MkRef__item__id",
        "typing_FStar.HyperStack.poppable", "typing_FStar.Map.contains",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.line",
      1,
      0,
      1,
      [
        "@query", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.v",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.idx",
        "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.UInt32.t",
        "lemma_FStar.Buffer.lemma_size",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_5fd76f96dd8842f1d4e9ef690b5c4ee7",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.UInt32.v"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.line",
      2,
      0,
      1,
      [
        "@query", "equation_FStar.Buffer.as_seq",
        "equation_FStar.Buffer.buffer", "equation_FStar.UInt32.add_mod",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.v",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.idx",
        "equation_Hacl.Impl.Salsa20.op_Less_Less_Less",
        "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.UInt32.t",
        "equation_Spec.Lib.op_Less_Less_Less",
        "equation_Spec.Lib.rotate_left", "equation_Spec.Salsa20.line",
        "equation_Spec.Salsa20.state",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "interpretation_Tm_abs_d33f818c2183bdf72245cda48ae8a8c3",
        "refinement_interpretation_Tm_refine_08b7b502ca9d52863cc90a1acbeae1a4",
        "refinement_interpretation_Tm_refine_5fd76f96dd8842f1d4e9ef690b5c4ee7",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "token_correspondence_Spec.Salsa20.line"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.quarter_round",
      1,
      0,
      1,
      [
        "@query", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.v",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.idx",
        "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.UInt32.t",
        "lemma_FStar.Buffer.lemma_size",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_5fd76f96dd8842f1d4e9ef690b5c4ee7",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.UInt32.v"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.quarter_round",
      2,
      0,
      1,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing",
        "data_elim_FStar.UInt32.Mk", "equation_FStar.Buffer.as_seq",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.contains",
        "equation_FStar.Buffer.live",
        "equation_FStar.HyperHeap.contains_ref",
        "equation_FStar.HyperStack.contains", "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.UInt32.v",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.UInt32.t", "equation_Spec.Lib.op_At",
        "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant2",
        "equation_Spec.Salsa20.quarter_round", "equation_Spec.Salsa20.state",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "function_token_typing_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant2",
        "kinding_FStar.UInt32.t_@tok",
        "lemma_FStar.Buffer.lemma_modifies_1_trans",
        "lemma_FStar.HyperStack.lemma_equal_domains_trans",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt32.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.UInt32.Mk_v",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "token_correspondence_Spec.Lib.op_At",
        "token_correspondence_Spec.Salsa20.line",
        "token_correspondence_Spec.Salsa20.quarter_round"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.column_round",
      1,
      0,
      1,
      [
        "@query", "equation_FStar.UInt32.t",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.UInt32.t",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.column_round",
      2,
      0,
      1,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing",
        "data_elim_FStar.UInt32.Mk", "data_elim_Spec.CTR.Mkblock_cipher_ctx",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.contains", "equation_FStar.Buffer.live",
        "equation_FStar.HyperHeap.contains_ref",
        "equation_FStar.HyperStack.contains", "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.UInt32.v",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.UInt32.t", "equation_Prims.nat",
        "equation_Spec.Chacha20.blocklen",
        "equation_Spec.Chacha20.chacha20_ctx",
        "equation_Spec.Chacha20.keylen", "equation_Spec.Chacha20.noncelen",
        "equation_Spec.Lib.op_At", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.column_round",
        "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant2",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.state",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "function_token_typing_Spec.Chacha20.chacha20_ctx",
        "function_token_typing_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant2",
        "function_token_typing_Spec.Salsa20.salsa20_ctx",
        "kinding_FStar.UInt32.t_@tok",
        "lemma_FStar.Buffer.lemma_modifies_1_trans",
        "lemma_FStar.HyperStack.lemma_equal_domains_trans",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_FStar.UInt32.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.UInt32.Mk_v",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "token_correspondence_Spec.Lib.op_At",
        "token_correspondence_Spec.Salsa20.quarter_round"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.row_round",
      1,
      0,
      1,
      [
        "@query", "equation_FStar.UInt32.t",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.UInt32.t",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.row_round",
      2,
      0,
      1,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing",
        "data_elim_FStar.UInt32.Mk", "data_elim_Spec.CTR.Mkblock_cipher_ctx",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.contains", "equation_FStar.Buffer.live",
        "equation_FStar.HyperHeap.contains_ref",
        "equation_FStar.HyperStack.contains", "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.UInt32.v",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.UInt32.t", "equation_Prims.nat",
        "equation_Spec.Chacha20.blocklen",
        "equation_Spec.Chacha20.chacha20_ctx",
        "equation_Spec.Chacha20.keylen", "equation_Spec.Chacha20.noncelen",
        "equation_Spec.Lib.op_At", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant2",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.row_round",
        "equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.state",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "function_token_typing_Spec.Chacha20.chacha20_ctx",
        "function_token_typing_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant2",
        "function_token_typing_Spec.Salsa20.salsa20_ctx",
        "kinding_FStar.UInt32.t_@tok",
        "lemma_FStar.Buffer.lemma_modifies_1_trans",
        "lemma_FStar.HyperStack.lemma_equal_domains_trans",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_FStar.UInt32.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.UInt32.Mk_v",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "token_correspondence_Spec.Lib.op_At",
        "token_correspondence_Spec.Salsa20.quarter_round"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.double_round",
      1,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.double_round",
      2,
      0,
      1,
      [
        "@query", "equation_FStar.UInt32.t", "equation_Hacl.UInt32.t",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.double_round",
      3,
      0,
      1,
      [
        "@query", "equation_FStar.Buffer.as_seq", "equation_FStar.UInt32.t",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.UInt32.t",
        "equation_Spec.Lib.op_At", "equation_Spec.Salsa20.double_round",
        "equation_Spec.Salsa20.state",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "kinding_FStar.UInt32.t_@tok",
        "lemma_FStar.Buffer.lemma_modifies_1_trans",
        "lemma_FStar.HyperStack.lemma_equal_domains_trans",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "token_correspondence_Spec.Salsa20.column_round",
        "token_correspondence_Spec.Salsa20.row_round"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.rounds",
      1,
      0,
      1,
      [
        "@query", "equation_FStar.UInt32.t",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.UInt32.t",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.rounds",
      2,
      0,
      0,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing", "eq2-interp",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.length", "equation_FStar.Buffer.live",
        "equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.hh",
        "equation_FStar.HyperStack.is_in", "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.v", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.UInt32.t",
        "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Spec.Salsa20.double_round", "equation_Spec.Salsa20.rounds",
        "equation_Spec.Salsa20.state",
        "fuel_correspondence_Spec.Loops.repeat_spec.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "function_token_typing_FStar.Heap.emp",
        "function_token_typing_FStar.HyperHeap.root", "int_inversion",
        "interpretation_Tm_abs_3a9a578c04c66c96520c56e7a65552f5",
        "kinding_FStar.UInt32.t_@tok", "l_and-interp",
        "lemma_FStar.Buffer.lemma_modifies_1_trans",
        "lemma_FStar.Buffer.lemma_modifies_sub_1",
        "lemma_FStar.Buffer.lemma_size",
        "pretyping_6c86c071b92797cdf01eb016249a9465",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.HyperStack.HS_h",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_0dc1829dbc3c1d1c42b7a4e9e5c89884",
        "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_df782de28d42cc81ec07e4d442f8388e",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.HyperStack.__proj__HS__item__h",
        "typing_FStar.HyperStack.is_in", "typing_FStar.UInt32.v"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.sum_states",
      1,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.t",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.UInt32.t",
        "equation_Prims.nat",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.sum_states",
      2,
      0,
      1,
      [
        "@query", "equation_FStar.UInt32.t",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.UInt32.t",
        "refinement_interpretation_Tm_refine_790772d82e6c5382184d4482620e08ca",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.sum_states",
      3,
      0,
      1,
      [
        "@query", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.length", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt32.t",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.UInt32.t", "kinding_FStar.UInt32.t_@tok",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_790772d82e6c5382184d4482620e08ca",
        "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.UInt32.v"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.copy_state",
      1,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0
    ],
    [ "Hacl.Impl.Salsa20.copy_state", 2, 0, 1, [ "@query" ], 0 ],
    [
      "Hacl.Impl.Salsa20.copy_state",
      3,
      0,
      1,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing",
        "data_elim_FStar.UInt32.Mk", "equation_FStar.Buffer.as_seq",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.contains",
        "equation_FStar.Buffer.equal", "equation_FStar.Buffer.length",
        "equation_FStar.Buffer.live",
        "equation_FStar.HyperHeap.contains_ref",
        "equation_FStar.HyperStack.contains", "equation_FStar.Int16.n",
        "equation_FStar.List.Tot.Base.test_sort",
        "equation_FStar.Seq.banana", "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_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.UInt32.t",
        "equation_Prims._assert", "equation_Prims.nat",
        "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant2",
        "fuel_correspondence_FStar.Seq.Base.slice.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "function_token_typing_FStar.Int16.n",
        "function_token_typing_FStar.List.Tot.Base.test_sort",
        "function_token_typing_FStar.Seq.banana",
        "function_token_typing_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant2", "int_inversion",
        "kinding_FStar.UInt32.t_@tok",
        "lemma_FStar.Buffer.lemma_disjoint_symm",
        "lemma_FStar.Buffer.no_upd_lemma_1",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_0c39788a35c67ccb2b6c008a42650895",
        "refinement_interpretation_Tm_refine_5ec5b64a8a200c47ed44dad76f0de705",
        "refinement_interpretation_Tm_refine_61b49facf2d28ca9c11c0eebf24ee9f9",
        "refinement_interpretation_Tm_refine_790772d82e6c5382184d4482620e08ca",
        "refinement_interpretation_Tm_refine_7e3beb6acccffb41919f80afab550fdd",
        "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
        "refinement_interpretation_Tm_refine_a341af39caff669bb0afe0b53bc92beb",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.Buffer.as_seq", "typing_FStar.UInt32.v",
        "unit_inversion"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.log_t_",
      1,
      0,
      1,
      [
        "@query", "assumption_FStar.Seq.Base.seq_haseq",
        "assumption_FStar.UInt8.t__haseq", "equation_FStar.UInt8.t",
        "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.key",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce",
        "equation_Spec.Salsa20.noncelen",
        "haseqTm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "kinding_FStar.UInt8.t_@tok"
      ],
      0
    ],
    [ "Hacl.Impl.Salsa20.__proj__MkLog__item__k", 1, 0, 1, [ "@query" ], 0 ],
    [ "Hacl.Impl.Salsa20.__proj__MkLog__item__n", 1, 0, 1, [ "@query" ], 0 ],
    [
      "Hacl.Impl.Salsa20.u64_of_u32s",
      1,
      0,
      1,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing",
        "data_elim_FStar.UInt32.Mk", "data_elim_FStar.UInt64.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.UInt32.v",
        "equation_FStar.UInt64.logor", "equation_FStar.UInt64.n",
        "equation_FStar.UInt64.shift_left", "equation_FStar.UInt64.t",
        "equation_FStar.UInt64.v", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Salsa20.constant0",
        "equation_Spec.Salsa20.constant2",
        "fuel_correspondence_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt64.n",
        "function_token_typing_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant2", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.UInt64.Mk_v",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_4e1413d692887900b561793d613871a2",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.Int.Cast.uint32_to_uint64", "typing_Prims.pow2"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.u64_of_u32s",
      2,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.u64_of_u32s",
      3,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.low32_of_u64",
      1,
      0,
      1,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.low32_of_u64",
      2,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.low32_of_u64",
      3,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.high32_of_u64",
      1,
      0,
      1,
      [
        "@query", "b2t_def", "data_elim_FStar.UInt32.Mk",
        "data_elim_FStar.UInt64.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_FStar.UInt64.n",
        "equation_FStar.UInt64.shift_right", "equation_FStar.UInt64.t",
        "equation_FStar.UInt64.v", "equation_Spec.Salsa20.constant0",
        "equation_Spec.Salsa20.constant2",
        "fuel_correspondence_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_FStar.UInt64.t_",
        "function_token_typing_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant2", "int_inversion",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt64.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.UInt64.Mk_v",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.high32_of_u64",
      2,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.high32_of_u64",
      3,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.invariant",
      1,
      0,
      1,
      [
        "@query", "equation_FStar.UInt32.t",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.UInt32.t", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_invariant",
      1,
      0,
      1,
      [
        "@query", "equation_FStar.UInt32.t", "equation_FStar.UInt8.t",
        "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.nonce",
        "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.state",
        "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_77fc284c2baaf580f00529ed84779843",
        "refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "typing_FStar.Seq.Base.length"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_invariant",
      2,
      0,
      1,
      [
        "@query", "equation_FStar.Mul.op_Star", "equation_FStar.UInt32.t",
        "equation_FStar.UInt64.t", "equation_FStar.UInt8.n",
        "equation_FStar.UInt8.t", "equation_Hacl.Cast.uint32_to_sint32",
        "equation_Hacl.Impl.Salsa20.high32_of_u64",
        "equation_Hacl.Impl.Salsa20.low32_of_u64",
        "equation_Hacl.Spec.Endianness.h64_to_u64", "equation_Hacl.UInt32.t",
        "equation_Hacl.UInt64.v", "equation_Prims.nat",
        "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.constant0",
        "equation_Spec.Salsa20.constant1", "equation_Spec.Salsa20.constant2",
        "equation_Spec.Salsa20.constant3", "equation_Spec.Salsa20.key",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce",
        "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.setup",
        "equation_Spec.Salsa20.state",
        "fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented",
        "function_token_typing_FStar.UInt8.n", "int_inversion",
        "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_2faf719c1498ed3501c17cc4a68989f0",
        "refinement_interpretation_Tm_refine_54c03c78d7539eae7ee3b6a012705328",
        "refinement_interpretation_Tm_refine_6619a3dbde5eda0c700823def7b7277e",
        "refinement_interpretation_Tm_refine_895213615ca428b66504b64c66c6d542",
        "refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d0b65c2e63980ded22de9fa4e6f18a29",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "refinement_interpretation_Tm_refine_ec8c52b60e5c33b3ae66e4063643ec19",
        "refinement_interpretation_Tm_refine_f91d5e2823046c84a18bf88075ce3a65",
        "typing_FStar.Seq.Base.length",
        "typing_Hacl.Impl.Salsa20.high32_of_u64",
        "typing_Hacl.Impl.Salsa20.low32_of_u64",
        "typing_Spec.Lib.uint32s_from_le"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_state_counter",
      1,
      0,
      1,
      [
        "@query", "b2t_def", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.t",
        "equation_FStar.UInt8.t", "equation_Spec.Lib.lbytes",
        "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.key",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce",
        "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.setup",
        "equation_Spec.Salsa20.state",
        "fuel_guarded_inversion_FStar.Seq.Base.seq", "int_inversion",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "typing_Spec.Salsa20.setup"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_state_counter",
      2,
      0,
      1,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing",
        "data_elim_FStar.UInt32.Mk", "data_elim_Spec.CTR.Mkblock_cipher_ctx",
        "equation_FStar.Mul.op_Star", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.shift_right", "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.UInt32.v", "equation_FStar.UInt64.n",
        "equation_FStar.UInt64.shift_right", "equation_FStar.UInt64.t",
        "equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v",
        "equation_FStar.UInt8.n", "equation_FStar.UInt8.t",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant1",
        "equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.constant3",
        "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.key",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.setup",
        "equation_Spec.Salsa20.state",
        "fuel_correspondence_Prims.pow2.fuel_instrumented",
        "fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt64.n",
        "function_token_typing_FStar.UInt8.n",
        "function_token_typing_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant1",
        "function_token_typing_Spec.Salsa20.constant2",
        "function_token_typing_Spec.Salsa20.constant3",
        "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion",
        "int_typing", "kinding_FStar.UInt32.t_@tok",
        "kinding_FStar.UInt8.t_@tok", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt.shift_right_value_lemma",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.UInt32.Mk_v",
        "projection_inverse_FStar.UInt64.Mk_v",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_895213615ca428b66504b64c66c6d542",
        "refinement_interpretation_Tm_refine_a5119fe68204e29c3bd16109f4988da3",
        "refinement_interpretation_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
        "refinement_interpretation_Tm_refine_b560551048d2e17324f021503ddc4232",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c1783956166b1754d457b3ddaaeb9cc5",
        "refinement_interpretation_Tm_refine_cf7d62afa1b585a00fa67c5958e52ab2",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "refinement_interpretation_Tm_refine_ec8c52b60e5c33b3ae66e4063643ec19",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.Int.Cast.uint64_to_uint32", "typing_FStar.Mul.op_Star",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_FStar.UInt.shift_right", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v", "typing_FStar.UInt64.shift_right",
        "typing_FStar.UInt64.uint_to_t", "typing_Seq.Create.create_16",
        "typing_Spec.Lib.uint32s_from_le", "typing_Spec.Salsa20.setup",
        "unit_typing"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_u64_of_u32s",
      1,
      0,
      1,
      [
        "@query", "b2t_def", "data_elim_FStar.UInt32.Mk",
        "equation_FStar.Mul.op_Star", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.logor", "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.UInt32.v", "equation_FStar.UInt64.logor",
        "equation_FStar.UInt64.n", "equation_FStar.UInt64.t",
        "equation_FStar.UInt64.v",
        "equation_Hacl.Impl.Salsa20.high32_of_u64",
        "equation_Hacl.Impl.Salsa20.low32_of_u64",
        "equation_Hacl.Impl.Salsa20.u64_of_u32s", "equation_Prims.nat",
        "equation_Spec.Salsa20.constant2",
        "fuel_correspondence_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_Spec.Salsa20.constant2", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.UInt64.Mk_v",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_19ef25f2e2d3d73de8cb0dc4c23167bd",
        "refinement_interpretation_Tm_refine_895213615ca428b66504b64c66c6d542",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d0b65c2e63980ded22de9fa4e6f18a29",
        "typing_FStar.UInt64.v", "typing_Hacl.Impl.Salsa20.high32_of_u64",
        "typing_Hacl.Impl.Salsa20.low32_of_u64",
        "typing_Hacl.Impl.Salsa20.u64_of_u32s"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_u64_of_u32s",
      2,
      0,
      1,
      [
        "@query", "assumption_FStar.UInt32.t__haseq",
        "equation_FStar.UInt32.t"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_u64_of_u32s",
      3,
      0,
      1,
      [
        "@query", "assumption_FStar.UInt32.t__haseq",
        "equation_FStar.UInt32.t"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_u64_of_u32s",
      4,
      0,
      1,
      [
        "@query", "assumption_FStar.UInt32.t__haseq",
        "equation_FStar.UInt32.t"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_u64_of_u32s",
      5,
      0,
      1,
      [
        "@query", "assumption_FStar.UInt32.t__haseq",
        "equation_FStar.UInt32.t"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_u64_of_u32s",
      6,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_u64_of_u32s",
      7,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_e5e09b9db68eee1607b2e382893a4997",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_core",
      1,
      0,
      0,
      [
        "@query", "equation_FStar.UInt32.t",
        "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.invariant",
        "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.UInt32.t",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5823fb0a569551a2a3a2765139ac8d74",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_core",
      2,
      0,
      0,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing",
        "constructor_distinct_Prims.Mktuple2",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.equal",
        "equation_FStar.Buffer.get", "equation_FStar.Buffer.length",
        "equation_FStar.Ghost.elift1", "equation_FStar.Ghost.reveal",
        "equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.hh",
        "equation_FStar.HyperStack.is_in", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.shift_right", "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.UInt32.v", "equation_FStar.UInt64.logor",
        "equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_right",
        "equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t",
        "equation_FStar.UInt64.v", "equation_FStar.UInt8.n",
        "equation_Hacl.Cast.uint32_to_sint32",
        "equation_Hacl.Cast.uint64_to_sint64",
        "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.invariant",
        "equation_Hacl.Impl.Salsa20.log_t",
        "equation_Hacl.Impl.Salsa20.low32_of_u64",
        "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.Impl.Salsa20.u64_of_u32s",
        "equation_Hacl.Spec.Endianness.h32_to_u32",
        "equation_Hacl.Spec.Endianness.h64_to_u64", "equation_Hacl.UInt32.t",
        "equation_Hacl.UInt64.t", "equation_Hacl.UInt64.v",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Salsa20.salsa20_core", "equation_Spec.Salsa20.setup",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "fuel_guarded_inversion_FStar.UInt64.t_",
        "function_token_typing_FStar.Heap.emp",
        "function_token_typing_FStar.HyperHeap.root",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt64.n",
        "function_token_typing_FStar.UInt8.n", "int_typing",
        "interpretation_Tm_abs_0047ad650fe3e711b278b738866d90c7",
        "kinding_FStar.UInt32.t_@tok",
        "kinding_Hacl.Impl.Salsa20.log_t_@tok",
        "lemma_FStar.Buffer.lemma_disjoint_symm",
        "lemma_FStar.Buffer.lemma_modifies_1_1",
        "lemma_FStar.Buffer.lemma_modifies_1_trans",
        "lemma_FStar.Buffer.lemma_modifies_2_1",
        "lemma_FStar.Buffer.no_upd_lemma_1",
        "lemma_FStar.HyperStack.lemma_equal_domains_trans",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2",
        "lemma_FStar.UInt.shift_right_value_lemma",
        "pretyping_6c86c071b92797cdf01eb016249a9465",
        "pretyping_a87e903bbc455531fa4b8b47a243ed22",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.HyperStack.HS_h",
        "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v",
        "proj_equation_Hacl.Impl.Salsa20.MkLog_k",
        "proj_equation_Hacl.Impl.Salsa20.MkLog_n",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.UInt32.Mk_v",
        "projection_inverse_FStar.UInt64.Mk_v",
        "projection_inverse_Prims.Mktuple2__1",
        "projection_inverse_Prims.Mktuple2__2",
        "projection_inverse_Prims.Mktuple2__a",
        "projection_inverse_Prims.Mktuple2__b",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_0dc1829dbc3c1d1c42b7a4e9e5c89884",
        "refinement_interpretation_Tm_refine_19ef25f2e2d3d73de8cb0dc4c23167bd",
        "refinement_interpretation_Tm_refine_5823fb0a569551a2a3a2765139ac8d74",
        "refinement_interpretation_Tm_refine_62cc9074e48a2f0ad3bde666284efad8",
        "refinement_interpretation_Tm_refine_6619a3dbde5eda0c700823def7b7277e",
        "refinement_interpretation_Tm_refine_6c4a32e73a864b089a00f3a625fffc64",
        "refinement_interpretation_Tm_refine_70421b53c2f82b8a1f874a6681f679e0",
        "refinement_interpretation_Tm_refine_7e3beb6acccffb41919f80afab550fdd",
        "refinement_interpretation_Tm_refine_895213615ca428b66504b64c66c6d542",
        "refinement_interpretation_Tm_refine_8ee8ddbbc8392bdb157fc0f0cc579d57",
        "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_d0b65c2e63980ded22de9fa4e6f18a29",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Tm_refine_ec8c52b60e5c33b3ae66e4063643ec19",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.Buffer.__proj__MkBuffer__item__idx",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Ghost.reveal",
        "typing_FStar.HyperStack.__proj__HS__item__h",
        "typing_FStar.HyperStack.is_in", "typing_FStar.UInt32.v",
        "typing_FStar.UInt64.v", "typing_Hacl.Cast.uint32_to_sint32",
        "typing_Hacl.Impl.Salsa20.high32_of_u64",
        "typing_Hacl.Impl.Salsa20.low32_of_u64",
        "typing_Hacl.Impl.Salsa20.u64_of_u32s"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_block",
      1,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [ "Hacl.Impl.Salsa20.salsa20_block", 2, 0, 1, [ "@query" ], 0 ],
    [
      "Hacl.Impl.Salsa20.salsa20_block",
      3,
      0,
      0,
      [
        "@query", "assumption_FStar.HyperHeap.HasEq_rid", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.Buffer.as_seq",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.contains",
        "equation_FStar.Buffer.content", "equation_FStar.Buffer.equal",
        "equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.length",
        "equation_FStar.Buffer.live", "equation_FStar.Buffer.sel",
        "equation_FStar.Ghost.reveal", "equation_FStar.HyperHeap.sel",
        "equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.contains",
        "equation_FStar.HyperStack.equal_domains",
        "equation_FStar.HyperStack.frameOf",
        "equation_FStar.HyperStack.fresh_frame",
        "equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_tip",
        "equation_FStar.HyperStack.live_region",
        "equation_FStar.HyperStack.pop",
        "equation_FStar.HyperStack.poppable",
        "equation_FStar.HyperStack.popped",
        "equation_FStar.HyperStack.remove_elt",
        "equation_FStar.HyperStack.sel", "equation_FStar.Mul.op_Star",
        "equation_FStar.ST.inline_stack_inv", "equation_FStar.Set.eqtype",
        "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.UInt32.v", "equation_FStar.UInt64.logor",
        "equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_right",
        "equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t",
        "equation_FStar.UInt64.v", "equation_FStar.UInt8.t",
        "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.high32_of_u64",
        "equation_Hacl.Impl.Salsa20.invariant",
        "equation_Hacl.Impl.Salsa20.log_t",
        "equation_Hacl.Impl.Salsa20.low32_of_u64",
        "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.Impl.Salsa20.u64_of_u32s",
        "equation_Hacl.Impl.Salsa20.uint8_p",
        "equation_Hacl.Spec.Endianness.h32_to_u32", "equation_Hacl.UInt32.t",
        "equation_Hacl.UInt32.v", "equation_Hacl.UInt8.t",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.constant0",
        "equation_Spec.Salsa20.constant1", "equation_Spec.Salsa20.constant2",
        "equation_Spec.Salsa20.constant3", "equation_Spec.Salsa20.key",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_block", "equation_Spec.Salsa20.setup",
        "fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.reference",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "fuel_guarded_inversion_FStar.UInt64.t_",
        "function_token_typing_FStar.Heap.emp",
        "function_token_typing_FStar.Heap.heap",
        "function_token_typing_FStar.HyperHeap.rid",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant1",
        "function_token_typing_Spec.Salsa20.constant2",
        "function_token_typing_Spec.Salsa20.constant3", "int_typing",
        "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok",
        "kinding_Hacl.Impl.Salsa20.log_t_@tok",
        "lemma_FStar.Buffer.lemma_disjoint_symm",
        "lemma_FStar.Buffer.lemma_equal_domains_2",
        "lemma_FStar.Buffer.lemma_fresh_poppable",
        "lemma_FStar.Buffer.lemma_live_disjoint",
        "lemma_FStar.Buffer.lemma_modifies_0_2_",
        "lemma_FStar.Buffer.lemma_modifies_2_1__",
        "lemma_FStar.Buffer.lemma_modifies_3_2_comm",
        "lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped",
        "lemma_FStar.Buffer.modifies_poppable_0",
        "lemma_FStar.Buffer.modifies_poppable_1",
        "lemma_FStar.Buffer.modifies_poppable_2",
        "lemma_FStar.Buffer.modifies_popped_3_2",
        "lemma_FStar.Buffer.no_upd_fresh",
        "lemma_FStar.Buffer.no_upd_lemma_0",
        "lemma_FStar.Buffer.no_upd_lemma_1",
        "lemma_FStar.Buffer.no_upd_lemma_2",
        "lemma_FStar.Buffer.no_upd_lemma_2_1",
        "lemma_FStar.Buffer.no_upd_popped",
        "lemma_FStar.HyperStack.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomUpd1",
        "lemma_FStar.Map.lemma_SelRestrict",
        "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement",
        "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
        "pretyping_6c86c071b92797cdf01eb016249a9465",
        "pretyping_a87e903bbc455531fa4b8b47a243ed22",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
        "primitive_Prims.op_disEquality",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.HyperStack.HS_h",
        "proj_equation_FStar.HyperStack.MkRef_id",
        "proj_equation_FStar.HyperStack.MkRef_ref",
        "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v",
        "proj_equation_Hacl.Impl.Salsa20.MkLog_k",
        "proj_equation_Hacl.Impl.Salsa20.MkLog_n",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.HyperStack.HS_h",
        "projection_inverse_FStar.UInt32.Mk_v",
        "projection_inverse_FStar.UInt64.Mk_v",
        "projection_inverse_Prims.Mktuple2__1",
        "projection_inverse_Prims.Mktuple2__2",
        "projection_inverse_Prims.Mktuple2__a",
        "projection_inverse_Prims.Mktuple2__b",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_0dc1829dbc3c1d1c42b7a4e9e5c89884",
        "refinement_interpretation_Tm_refine_19ef25f2e2d3d73de8cb0dc4c23167bd",
        "refinement_interpretation_Tm_refine_1acdc766b4c7c4eb63372045308d68b7",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_887952df5f5cce70cba88455191879c8",
        "refinement_interpretation_Tm_refine_895213615ca428b66504b64c66c6d542",
        "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
        "refinement_interpretation_Tm_refine_a5119fe68204e29c3bd16109f4988da3",
        "refinement_interpretation_Tm_refine_b560551048d2e17324f021503ddc4232",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_cf7d62afa1b585a00fa67c5958e52ab2",
        "refinement_interpretation_Tm_refine_d0b65c2e63980ded22de9fa4e6f18a29",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "refinement_interpretation_Tm_refine_de8123dd3e45084cdea7d9d0e7ffb100",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Tm_refine_ec8c52b60e5c33b3ae66e4063643ec19",
        "refinement_kinding_Tm_refine_a121f8bda6f05793d62ed0cfe5b942df",
        "typing_FStar.Buffer.__proj__MkBuffer__item__content",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.Buffer.idx", "typing_FStar.Ghost.reveal",
        "typing_FStar.HyperStack.__proj__HS__item__h",
        "typing_FStar.HyperStack.__proj__HS__item__tip",
        "typing_FStar.HyperStack.__proj__MkRef__item__id",
        "typing_FStar.HyperStack.poppable",
        "typing_FStar.HyperStack.remove_elt",
        "typing_FStar.Int.Cast.uint64_to_uint32",
        "typing_FStar.Map.contains", "typing_FStar.Map.domain",
        "typing_FStar.Map.restrict", "typing_FStar.Seq.Base.index",
        "typing_FStar.Seq.Base.length", "typing_FStar.Set.complement",
        "typing_FStar.Set.singleton", "typing_FStar.UInt.fits",
        "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
        "typing_FStar.UInt64.shift_right",
        "typing_Hacl.Impl.Salsa20.high32_of_u64",
        "typing_Hacl.Impl.Salsa20.low32_of_u64",
        "typing_Hacl.Impl.Salsa20.u64_of_u32s",
        "typing_Seq.Create.create_16", "typing_Spec.Lib.uint32s_from_le"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_block",
      4,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.alloc",
      1,
      0,
      1,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing",
        "data_elim_FStar.UInt32.Mk", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.live",
        "equation_FStar.HyperStack.is_stack_region",
        "equation_FStar.ST.inline_stack_inv", "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_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.UInt32.t",
        "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant2",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "function_token_typing_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant2",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.init",
      1,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.init",
      2,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.init",
      3,
      0,
      1,
      [
        "@query", "b2t_def", "bool_inversion",
        "constructor_distinct_Hacl.Impl.Salsa20.MkLog",
        "data_elim_Spec.CTR.Mkblock_cipher_ctx",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.contains", "equation_FStar.Buffer.equal",
        "equation_FStar.Buffer.live", "equation_FStar.Ghost.elift2",
        "equation_FStar.Ghost.hide", "equation_FStar.Ghost.reveal",
        "equation_FStar.HyperHeap.contains_ref",
        "equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.contains",
        "equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_in",
        "equation_FStar.Mul.op_Star", "equation_FStar.Seq.Base.index",
        "equation_FStar.Seq.Base.length", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt32.t",
        "equation_FStar.UInt64.n", "equation_FStar.UInt64.t",
        "equation_FStar.UInt64.v", "equation_FStar.UInt8.n",
        "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.invariant",
        "equation_Hacl.Impl.Salsa20.log_t",
        "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt32.t",
        "equation_Hacl.UInt8.t", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "fuel_correspondence_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.Heap.emp",
        "function_token_typing_FStar.HyperHeap.root",
        "function_token_typing_FStar.UInt64.n",
        "function_token_typing_FStar.UInt8.n",
        "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_63a15c105abe152a30c61ae574816e90",
        "interpretation_Tm_arrow_1b11ac8ae397ade469edcdbcfe2629d5",
        "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok",
        "lemma_FStar.Buffer.no_upd_lemma_1", "lemma_FStar.UInt.pow2_values",
        "pretyping_6c86c071b92797cdf01eb016249a9465",
        "pretyping_a87e903bbc455531fa4b8b47a243ed22",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.HyperStack.HS_h",
        "proj_equation_FStar.Seq.Base.MkSeq_l",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Hacl.Impl.Salsa20.MkLog_k",
        "projection_inverse_Hacl.Impl.Salsa20.MkLog_n",
        "refinement_interpretation_Tm_refine_0dc1829dbc3c1d1c42b7a4e9e5c89884",
        "refinement_interpretation_Tm_refine_162a3c2ee4d10c15b5e46cb5963460d6",
        "refinement_interpretation_Tm_refine_173c3f7fb931ea8e37f2cd554b93e659",
        "refinement_interpretation_Tm_refine_19ef25f2e2d3d73de8cb0dc4c23167bd",
        "refinement_interpretation_Tm_refine_96a28a851eecacef3e62c1298dc55be7",
        "refinement_interpretation_Tm_refine_b25bac71ace031ea1b4048c58d6ef05a",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_d0248a37b555c45264d4be3b1e2a8bff",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Tm_refine_ec8c52b60e5c33b3ae66e4063643ec19",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.Buffer.length",
        "typing_FStar.HyperStack.__proj__HS__item__h",
        "typing_FStar.HyperStack.is_in", "typing_FStar.List.Tot.Base.index",
        "typing_FStar.Seq.Base.__proj__MkSeq__item__l",
        "typing_FStar.Seq.Base.index",
        "typing_Hacl.Impl.Salsa20.u64_of_u32s", "typing_Prims.pow2"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.init",
      4,
      0,
      0,
      [
        "@query", "b2t_def", "constructor_distinct_Hacl.Impl.Salsa20.MkLog",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.equal", "equation_FStar.Buffer.length",
        "equation_FStar.Ghost.elift2", "equation_FStar.Ghost.hide",
        "equation_FStar.Ghost.reveal", "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.UInt32.t", "equation_FStar.UInt32.uint_to_t",
        "equation_FStar.UInt32.v", "equation_FStar.UInt64.n",
        "equation_FStar.UInt64.shift_right", "equation_FStar.UInt64.t",
        "equation_FStar.UInt64.v", "equation_FStar.UInt8.n",
        "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.invariant",
        "equation_Hacl.Impl.Salsa20.log_t",
        "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.Impl.Salsa20.u64_of_u32s",
        "equation_Hacl.Impl.Salsa20.uint8_p",
        "equation_Hacl.Spec.Endianness.h32_to_u32", "equation_Hacl.UInt32.t",
        "equation_Hacl.UInt32.v", "equation_Hacl.UInt8.t",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.constant0",
        "equation_Spec.Salsa20.constant1", "equation_Spec.Salsa20.constant2",
        "equation_Spec.Salsa20.constant3", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.setup",
        "fuel_correspondence_Prims.pow2.fuel_instrumented",
        "fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "function_token_typing_FStar.UInt64.n",
        "function_token_typing_FStar.UInt8.n",
        "function_token_typing_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant1",
        "function_token_typing_Spec.Salsa20.constant2",
        "function_token_typing_Spec.Salsa20.constant3", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_63a15c105abe152a30c61ae574816e90",
        "interpretation_Tm_arrow_1b11ac8ae397ade469edcdbcfe2629d5",
        "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok",
        "lemma_FStar.Buffer.no_upd_lemma_1", "lemma_FStar.UInt.pow2_values",
        "pretyping_a87e903bbc455531fa4b8b47a243ed22",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.UInt32.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Hacl.Impl.Salsa20.MkLog_k",
        "projection_inverse_Hacl.Impl.Salsa20.MkLog_n",
        "refinement_interpretation_Tm_refine_162a3c2ee4d10c15b5e46cb5963460d6",
        "refinement_interpretation_Tm_refine_173c3f7fb931ea8e37f2cd554b93e659",
        "refinement_interpretation_Tm_refine_19ef25f2e2d3d73de8cb0dc4c23167bd",
        "refinement_interpretation_Tm_refine_895213615ca428b66504b64c66c6d542",
        "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
        "refinement_interpretation_Tm_refine_a5119fe68204e29c3bd16109f4988da3",
        "refinement_interpretation_Tm_refine_b25bac71ace031ea1b4048c58d6ef05a",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_cf7d62afa1b585a00fa67c5958e52ab2",
        "refinement_interpretation_Tm_refine_d0248a37b555c45264d4be3b1e2a8bff",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Tm_refine_ec8c52b60e5c33b3ae66e4063643ec19",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.Buffer.length",
        "typing_FStar.Int.Cast.uint64_to_uint32", "typing_FStar.Mul.op_Star",
        "typing_FStar.Seq.Base.index", "typing_FStar.UInt64.shift_right",
        "typing_Hacl.Impl.Salsa20.u64_of_u32s", "typing_Prims.pow2",
        "typing_Seq.Create.create_16", "typing_Spec.Lib.uint32s_from_le"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.init",
      5,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.init",
      6,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.init",
      7,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.init",
      8,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.init",
      9,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.init",
      10,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1",
      1,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1",
      2,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1",
      3,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1",
      4,
      0,
      0,
      [
        "@query", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.contains", "equation_FStar.Buffer.live",
        "equation_FStar.HyperHeap.contains_ref",
        "equation_FStar.HyperStack.contains", "equation_FStar.Mul.op_Star",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt32.t",
        "equation_FStar.UInt64.n", "equation_FStar.UInt64.t",
        "equation_FStar.UInt64.v", "equation_FStar.UInt8.t",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt8.t",
        "equation_Prims.nat", "equation_Spec.CTR.counter",
        "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.block",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.counter",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_block",
        "equation_Spec.Salsa20.salsa20_ctx",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_guarded_inversion_FStar.UInt64.t_", "int_inversion",
        "int_typing", "kinding_FStar.UInt8.t_@tok",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_Tm_refine_0c39788a35c67ccb2b6c008a42650895",
        "refinement_interpretation_Tm_refine_60973e758229a14ccd951c4bd45d0b29",
        "refinement_interpretation_Tm_refine_6925cb0f165c2ed09ea63ef366099574",
        "refinement_interpretation_Tm_refine_a12156fd6d3750813ff3acbaa0cc9e82",
        "refinement_interpretation_Tm_refine_b44e188053a2b04fca2a9e07d2726af0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "typing_FStar.Buffer.length", "typing_FStar.Seq.Base.length",
        "typing_Spec.Salsa20.salsa20_block"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1",
      5,
      1,
      1,
      [
        "@query", "equation_FStar.Buffer.as_seq",
        "equation_FStar.Buffer.buffer", "equation_FStar.UInt32.t",
        "equation_FStar.UInt64.v", "equation_FStar.UInt8.t",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt8.t",
        "equation_Spec.CTR.xor", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_cipher",
        "equation_Spec.Salsa20.salsa20_ctx",
        "equation_with_fuel_Spec.CTR.counter_mode.fuel_instrumented",
        "equation_with_fuel_Spec.Loops.seq_map2.fuel_instrumented",
        "fuel_correspondence_Spec.CTR.counter_mode.fuel_instrumented",
        "fuel_correspondence_Spec.Loops.seq_map2.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "kinding_FStar.UInt8.t_@tok", "primitive_Prims.op_LessThan",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "refinement_interpretation_Tm_refine_7e3beb6acccffb41919f80afab550fdd",
        "refinement_interpretation_Tm_refine_a12156fd6d3750813ff3acbaa0cc9e82",
        "refinement_interpretation_Tm_refine_b44e188053a2b04fca2a9e07d2726af0",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "token_correspondence_Spec.Salsa20.salsa20_block",
        "typing_FStar.Buffer.as_seq", "unit_typing"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_2",
      1,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_2",
      2,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_2",
      3,
      0,
      0,
      [
        "@query", "b2t_def", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.contains", "equation_FStar.Buffer.live",
        "equation_FStar.HyperHeap.contains_ref",
        "equation_FStar.HyperStack.contains", "equation_FStar.Mul.op_Star",
        "equation_FStar.Seq.Properties.split", "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.t", "equation_FStar.UInt64.n",
        "equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
        "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p",
        "equation_Hacl.UInt8.t", "equation_Prims.nat",
        "equation_Spec.CTR.counter", "equation_Spec.Lib.lbytes",
        "equation_Spec.Salsa20.block", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_block",
        "equation_Spec.Salsa20.salsa20_ctx",
        "fuel_correspondence_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_guarded_inversion_FStar.UInt64.t_",
        "function_token_typing_FStar.UInt64.n",
        "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_typing",
        "kinding_FStar.UInt8.t_@tok", "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Mktuple2__1",
        "projection_inverse_Prims.Mktuple2__2",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_0c39788a35c67ccb2b6c008a42650895",
        "refinement_interpretation_Tm_refine_49a4727577b21ead5b4f874342629b71",
        "refinement_interpretation_Tm_refine_6925cb0f165c2ed09ea63ef366099574",
        "refinement_interpretation_Tm_refine_b44e188053a2b04fca2a9e07d2726af0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "typing_FStar.Buffer.length", "typing_FStar.UInt64.v",
        "typing_Spec.CTR.__proj__Mkblock_cipher_ctx__item__counterbits",
        "typing_Spec.Salsa20.salsa20_block"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_2",
      4,
      1,
      1,
      [
        "@query", "b2t_def", "bool_inversion",
        "constructor_distinct_Prims.Mktuple2",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Seq.Base.op_At_Bar",
        "equation_FStar.Seq.Properties.split", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt32.t",
        "equation_FStar.UInt64.v", "equation_FStar.UInt8.t",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt8.t",
        "equation_Prims.nat", "equation_Spec.CTR.xor",
        "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_block",
        "equation_Spec.Salsa20.salsa20_cipher",
        "equation_Spec.Salsa20.salsa20_ctx",
        "equation_with_fuel_Spec.CTR.counter_mode.fuel_instrumented",
        "fuel_correspondence_Spec.CTR.counter_mode.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_irrelevance_Spec.CTR.counter_mode.fuel_instrumented",
        "kinding_FStar.UInt8.t_@tok", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "proj_equation_FStar.UInt32.Mk_v",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.UInt32.Mk_v",
        "projection_inverse_Prims.Mktuple2__1",
        "projection_inverse_Prims.Mktuple2__2",
        "projection_inverse_Prims.Mktuple2__a",
        "projection_inverse_Prims.Mktuple2__b",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_49a4727577b21ead5b4f874342629b71",
        "refinement_interpretation_Tm_refine_7e3beb6acccffb41919f80afab550fdd",
        "refinement_interpretation_Tm_refine_b44e188053a2b04fca2a9e07d2726af0",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "token_correspondence_Spec.Salsa20.salsa20_block",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
        "typing_FStar.UInt32.v", "unit_typing"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0",
      1,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0",
      2,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0",
      3,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0",
      4,
      0,
      1,
      [
        "@query", "equation_FStar.Buffer.buffer",
        "equation_FStar.Mul.op_Star", "equation_FStar.UInt64.n",
        "equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
        "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p",
        "equation_Hacl.UInt8.t", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Multiply",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_Tm_refine_6925cb0f165c2ed09ea63ef366099574",
        "refinement_interpretation_Tm_refine_b44e188053a2b04fca2a9e07d2726af0",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0",
      5,
      1,
      1,
      [
        "@query", "equation_FStar.Buffer.as_seq",
        "equation_FStar.Buffer.buffer",
        "equation_FStar.Seq.Base.createEmpty", "equation_FStar.UInt32.t",
        "equation_FStar.UInt64.v", "equation_FStar.UInt8.t",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt8.t",
        "equation_Prims.nat", "equation_Spec.Lib.lbytes",
        "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_cipher",
        "equation_Spec.Salsa20.salsa20_ctx",
        "equation_with_fuel_Spec.CTR.counter_mode.fuel_instrumented",
        "fuel_correspondence_Spec.CTR.counter_mode.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_guarded_inversion_FStar.Seq.Base.seq",
        "kinding_FStar.UInt8.t_@tok", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "primitive_Prims.op_Equality",
        "refinement_interpretation_Tm_refine_512ebc3f8c885e6f80a3b1e5baadda14",
        "refinement_interpretation_Tm_refine_61b49facf2d28ca9c11c0eebf24ee9f9",
        "refinement_interpretation_Tm_refine_7e3beb6acccffb41919f80afab550fdd",
        "refinement_interpretation_Tm_refine_b44e188053a2b04fca2a9e07d2726af0",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Seq.Base.createEmpty"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.update_last",
      1,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.update_last",
      2,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.update_last",
      3,
      0,
      0,
      [
        "@query", "equation_FStar.Buffer.length",
        "equation_FStar.Mul.op_Star", "equation_FStar.UInt64.n",
        "equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
        "equation_FStar.UInt8.t", "equation_Hacl.UInt8.t",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_Tm_refine_6925cb0f165c2ed09ea63ef366099574",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.update_last",
      4,
      0,
      0,
      [
        "@query", "assumption_FStar.HyperHeap.HasEq_rid", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.contains", "equation_FStar.Buffer.content",
        "equation_FStar.Buffer.equal", "equation_FStar.Buffer.frameOf",
        "equation_FStar.Buffer.idx", "equation_FStar.Buffer.includes",
        "equation_FStar.Buffer.length", "equation_FStar.Buffer.live",
        "equation_FStar.Buffer.sub", "equation_FStar.Ghost.reveal",
        "equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.contains",
        "equation_FStar.HyperStack.equal_domains",
        "equation_FStar.HyperStack.frameOf",
        "equation_FStar.HyperStack.fresh_frame",
        "equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_tip",
        "equation_FStar.HyperStack.live_region",
        "equation_FStar.HyperStack.pop",
        "equation_FStar.HyperStack.poppable",
        "equation_FStar.HyperStack.popped",
        "equation_FStar.HyperStack.remove_elt", "equation_FStar.Mul.op_Star",
        "equation_FStar.ST.inline_stack_inv", "equation_FStar.Set.eqtype",
        "equation_FStar.UInt.add", "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.add", "equation_FStar.UInt32.n",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
        "equation_FStar.UInt32.v", "equation_FStar.UInt64.n",
        "equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
        "equation_FStar.UInt8.n", "equation_FStar.UInt8.t",
        "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.invariant",
        "equation_Hacl.Impl.Salsa20.log_t",
        "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt32.t",
        "equation_Hacl.UInt8.t", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.CTR.counter", "equation_Spec.CTR.key",
        "equation_Spec.CTR.nonce", "equation_Spec.Lib.lbytes",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.key",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_cipher",
        "equation_Spec.Salsa20.salsa20_ctx",
        "fuel_correspondence_Prims.pow2.fuel_instrumented",
        "fuel_correspondence_Spec.Loops.seq_map2.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_guarded_inversion_FStar.HyperStack.reference",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "function_token_typing_FStar.Heap.emp",
        "function_token_typing_FStar.Heap.heap",
        "function_token_typing_FStar.HyperHeap.rid",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.n",
        "function_token_typing_Spec.Salsa20.salsa20_cipher",
        "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion",
        "int_typing", "kinding_FStar.UInt32.t_@tok",
        "kinding_FStar.UInt8.t_@tok", "kinding_Hacl.Impl.Salsa20.log_t_@tok",
        "lemma_FStar.Buffer.lemma_disjoint_symm",
        "lemma_FStar.Buffer.lemma_equal_domains_2",
        "lemma_FStar.Buffer.lemma_fresh_poppable",
        "lemma_FStar.Buffer.lemma_live_disjoint",
        "lemma_FStar.Buffer.lemma_modifies_0_2_",
        "lemma_FStar.Buffer.lemma_modifies_2_1__",
        "lemma_FStar.Buffer.lemma_modifies_3_2_comm",
        "lemma_FStar.Buffer.lemma_sub_spec", "lemma_FStar.Buffer.live_fresh",
        "lemma_FStar.Buffer.live_popped",
        "lemma_FStar.Buffer.modifies_poppable_1",
        "lemma_FStar.Buffer.modifies_popped_3_2",
        "lemma_FStar.Buffer.no_upd_fresh",
        "lemma_FStar.Buffer.no_upd_lemma_0",
        "lemma_FStar.Buffer.no_upd_lemma_1",
        "lemma_FStar.Buffer.no_upd_lemma_2_1",
        "lemma_FStar.Buffer.no_upd_popped",
        "lemma_FStar.HyperStack.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomUpd1",
        "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement",
        "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
        "lemma_FStar.UInt.pow2_values",
        "pretyping_6c86c071b92797cdf01eb016249a9465",
        "pretyping_a87e903bbc455531fa4b8b47a243ed22",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
        "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "proj_equation_FStar.Buffer.MkBuffer_idx",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.Buffer.MkBuffer_max_length",
        "proj_equation_FStar.HyperStack.HS_h",
        "proj_equation_FStar.HyperStack.MkRef_id",
        "proj_equation_FStar.UInt32.Mk_v",
        "proj_equation_Hacl.Impl.Salsa20.MkLog_k",
        "proj_equation_Hacl.Impl.Salsa20.MkLog_n",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Buffer.MkBuffer_idx",
        "projection_inverse_FStar.HyperStack.HS_h",
        "projection_inverse_Prims.Mktuple2__1",
        "projection_inverse_Prims.Mktuple2__2",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_0dc1829dbc3c1d1c42b7a4e9e5c89884",
        "refinement_interpretation_Tm_refine_27eb738955e795e5dd1cab5fe18de9a0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_44ea08795ee137b6e8aa1d28dc1aec75",
        "refinement_interpretation_Tm_refine_6925cb0f165c2ed09ea63ef366099574",
        "refinement_interpretation_Tm_refine_7874c81428902f5ef0683ead2eab5830",
        "refinement_interpretation_Tm_refine_790772d82e6c5382184d4482620e08ca",
        "refinement_interpretation_Tm_refine_7e3beb6acccffb41919f80afab550fdd",
        "refinement_interpretation_Tm_refine_a12156fd6d3750813ff3acbaa0cc9e82",
        "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_cdad18d4eea688c87fdef10082480b22",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "refinement_interpretation_Tm_refine_de8123dd3e45084cdea7d9d0e7ffb100",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_kinding_Tm_refine_a121f8bda6f05793d62ed0cfe5b942df",
        "typing_FStar.Buffer.__proj__MkBuffer__item__content",
        "typing_FStar.Buffer.__proj__MkBuffer__item__idx",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.content",
        "typing_FStar.Buffer.length", "typing_FStar.Ghost.reveal",
        "typing_FStar.HyperStack.__proj__HS__item__h",
        "typing_FStar.HyperStack.__proj__HS__item__tip",
        "typing_FStar.HyperStack.__proj__MkRef__item__id",
        "typing_FStar.HyperStack.poppable",
        "typing_FStar.HyperStack.remove_elt", "typing_FStar.Map.contains",
        "typing_FStar.Map.domain", "typing_FStar.Map.restrict",
        "typing_FStar.Set.complement", "typing_FStar.Set.intersect",
        "typing_FStar.Set.singleton", "typing_FStar.UInt32.v",
        "typing_FStar.UInt64.v", "typing_Prims.pow2",
        "typing_Spec.CTR.counter_mode"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.update",
      1,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.update",
      2,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.update",
      3,
      0,
      1,
      [
        "@query", "equation_FStar.Buffer.buffer", "equation_FStar.UInt64.n",
        "equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
        "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p",
        "equation_Hacl.UInt8.t", "equation_Spec.Lib.lbytes",
        "equation_Spec.Salsa20.block", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.key",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_cipher",
        "equation_Spec.Salsa20.salsa20_ctx",
        "function_token_typing_Spec.Salsa20.salsa20_block",
        "interpretation_Tm_arrow_f529f4c9cbc78ef050cefd8cf570168e",
        "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_BoxInt_proj_0",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_Tm_refine_25e6304b6a86439753488139c13484b5",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_ce01e3cba2a2fbf2c025b891a51ea08e",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "typing_FStar.UInt64.v"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.update",
      4,
      0,
      0,
      [
        "@query", "assumption_FStar.HyperHeap.HasEq_rid", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.contains", "equation_FStar.Buffer.content",
        "equation_FStar.Buffer.disjoint", "equation_FStar.Buffer.equal",
        "equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.idx",
        "equation_FStar.Buffer.includes", "equation_FStar.Buffer.length",
        "equation_FStar.Buffer.live", "equation_FStar.Buffer.sub",
        "equation_FStar.Ghost.reveal", "equation_FStar.HyperHeap.t",
        "equation_FStar.HyperStack.contains",
        "equation_FStar.HyperStack.equal_domains",
        "equation_FStar.HyperStack.frameOf",
        "equation_FStar.HyperStack.fresh_frame",
        "equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_tip",
        "equation_FStar.HyperStack.live_region",
        "equation_FStar.HyperStack.pop",
        "equation_FStar.HyperStack.poppable",
        "equation_FStar.HyperStack.popped",
        "equation_FStar.HyperStack.remove_elt", "equation_FStar.Mul.op_Star",
        "equation_FStar.ST.inline_stack_inv", "equation_FStar.Set.eqtype",
        "equation_FStar.UInt.add", "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.UInt16.n", "equation_FStar.UInt32.add",
        "equation_FStar.UInt32.n", "equation_FStar.UInt32.t",
        "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v",
        "equation_FStar.UInt64.n", "equation_FStar.UInt64.t",
        "equation_FStar.UInt64.v", "equation_FStar.UInt8.t",
        "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.high32_of_u64",
        "equation_Hacl.Impl.Salsa20.invariant",
        "equation_Hacl.Impl.Salsa20.log_t",
        "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.Impl.Salsa20.uint8_p",
        "equation_Hacl.Impl.Xor.Lemmas.u32",
        "equation_Hacl.Spec.Endianness.h32_to_u32", "equation_Hacl.UInt32.t",
        "equation_Hacl.UInt32.v", "equation_Hacl.UInt8.t",
        "equation_Prims.eqtype", "equation_Spec.Salsa20.salsa20_block",
        "equation_Spec.Salsa20.salsa20_cipher",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_guarded_inversion_FStar.HyperStack.reference",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "fuel_guarded_inversion_FStar.UInt64.t_",
        "function_token_typing_FStar.Heap.emp",
        "function_token_typing_FStar.Heap.heap",
        "function_token_typing_FStar.HyperHeap.rid",
        "function_token_typing_FStar.HyperStack.remove_elt",
        "function_token_typing_FStar.Set.complement",
        "function_token_typing_FStar.Set.singleton",
        "function_token_typing_FStar.UInt16.n", "int_inversion",
        "int_typing",
        "interpretation_Tm_arrow_4019e894ab4058a3164e2b8786c32b27",
        "interpretation_Tm_arrow_44cc1777afbdbed9bdd3d9b2ecbc41b2",
        "interpretation_Tm_arrow_f285bd18d16ed788dea4e9c47fb2243d",
        "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok",
        "kinding_Hacl.Impl.Salsa20.log_t_@tok",
        "lemma_FStar.Buffer.lemma_disjoint_symm",
        "lemma_FStar.Buffer.lemma_equal_domains_2",
        "lemma_FStar.Buffer.lemma_fresh_poppable",
        "lemma_FStar.Buffer.lemma_live_disjoint",
        "lemma_FStar.Buffer.lemma_modifies_0_2",
        "lemma_FStar.Buffer.lemma_modifies_1_1",
        "lemma_FStar.Buffer.lemma_modifies_1_trans",
        "lemma_FStar.Buffer.lemma_modifies_2_1_",
        "lemma_FStar.Buffer.lemma_modifies_2_1__",
        "lemma_FStar.Buffer.lemma_modifies_2_comm",
        "lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped",
        "lemma_FStar.Buffer.modifies_poppable_1",
        "lemma_FStar.Buffer.modifies_popped_3_2",
        "lemma_FStar.Buffer.modifies_subbuffer_1",
        "lemma_FStar.Buffer.modifies_subbuffer_2",
        "lemma_FStar.Buffer.no_upd_fresh",
        "lemma_FStar.Buffer.no_upd_lemma_0",
        "lemma_FStar.Buffer.no_upd_lemma_1",
        "lemma_FStar.Buffer.no_upd_lemma_2",
        "lemma_FStar.Buffer.no_upd_lemma_2_1",
        "lemma_FStar.Buffer.no_upd_popped",
        "lemma_FStar.HyperStack.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomUpd1",
        "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement",
        "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
        "lemma_FStar.UInt.pow2_values",
        "pretyping_6c86c071b92797cdf01eb016249a9465",
        "pretyping_a87e903bbc455531fa4b8b47a243ed22",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
        "primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "proj_equation_FStar.Buffer.MkBuffer_idx",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.Buffer.MkBuffer_max_length",
        "proj_equation_FStar.HyperStack.HS_h",
        "proj_equation_FStar.HyperStack.MkRef_id",
        "proj_equation_FStar.UInt32.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Buffer.MkBuffer_idx",
        "projection_inverse_FStar.HyperStack.HS_h",
        "projection_inverse_FStar.UInt32.Mk_v",
        "projection_inverse_Prims.Mktuple2__1",
        "projection_inverse_Prims.Mktuple2__2",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_0dc1829dbc3c1d1c42b7a4e9e5c89884",
        "refinement_interpretation_Tm_refine_19ef25f2e2d3d73de8cb0dc4c23167bd",
        "refinement_interpretation_Tm_refine_25e6304b6a86439753488139c13484b5",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_887952df5f5cce70cba88455191879c8",
        "refinement_interpretation_Tm_refine_895213615ca428b66504b64c66c6d542",
        "refinement_interpretation_Tm_refine_90c17150abf5cdb4d91f504ab07d9689",
        "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_cdad18d4eea688c87fdef10082480b22",
        "refinement_interpretation_Tm_refine_ce01e3cba2a2fbf2c025b891a51ea08e",
        "refinement_interpretation_Tm_refine_d0b65c2e63980ded22de9fa4e6f18a29",
        "refinement_interpretation_Tm_refine_de8123dd3e45084cdea7d9d0e7ffb100",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_kinding_Tm_refine_a121f8bda6f05793d62ed0cfe5b942df",
        "token_correspondence_FStar.HyperStack.remove_elt",
        "token_correspondence_FStar.Set.complement",
        "token_correspondence_FStar.Set.singleton",
        "token_correspondence_Spec.Salsa20.salsa20_block",
        "typing_FStar.Buffer.__proj__MkBuffer__item__content",
        "typing_FStar.Buffer.__proj__MkBuffer__item__idx",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.Buffer.content", "typing_FStar.Buffer.idx",
        "typing_FStar.Buffer.length", "typing_FStar.Ghost.reveal",
        "typing_FStar.HyperStack.__proj__HS__item__h",
        "typing_FStar.HyperStack.__proj__HS__item__tip",
        "typing_FStar.HyperStack.__proj__MkRef__item__id",
        "typing_FStar.HyperStack.poppable", "typing_FStar.Map.contains",
        "typing_FStar.Map.domain", "typing_FStar.Mul.op_Star",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_FStar.UInt64.v", "typing_Hacl.Impl.Salsa20.high32_of_u64",
        "typing_Hacl.Impl.Salsa20.low32_of_u64",
        "typing_Hacl.Impl.Salsa20.u64_of_u32s"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode",
      1,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_e0b8a7ce8790eaaca2b2e4fb4d625bad",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode",
      2,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode",
      3,
      0,
      1,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing",
        "data_elim_FStar.UInt32.Mk", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.contains", "equation_FStar.Buffer.includes",
        "equation_FStar.Buffer.length", "equation_FStar.Buffer.live",
        "equation_FStar.Buffer.offset", "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.sub", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt32.sub",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
        "equation_FStar.UInt32.v", "equation_FStar.UInt8.t",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt8.t",
        "equation_Spec.CTR.block", "equation_Spec.Lib.lbytes",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0",
        "equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.counter",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "fuel_correspondence_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_guarded_inversion_FStar.HyperStack.reference",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "function_token_typing_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant2", "int_inversion",
        "int_typing", "kinding_FStar.UInt8.t_@tok",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.Buffer.MkBuffer_max_length",
        "proj_equation_FStar.UInt32.Mk_v",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Buffer.MkBuffer_length",
        "projection_inverse_FStar.UInt32.Mk_v",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_109859f7283d820caaab3211c004ad66",
        "refinement_interpretation_Tm_refine_4eb09d73aa2900d334961d999d08edb6",
        "refinement_interpretation_Tm_refine_5460149187704503c8495590de3b3f5d",
        "refinement_interpretation_Tm_refine_907182d4e2170b57b8441f948a734676",
        "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
        "refinement_interpretation_Tm_refine_c1af962245efd987b248097ce687cffa",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "refinement_interpretation_Tm_refine_dca010ec7aae3ea7c12c586af7fbfc77",
        "refinement_interpretation_Tm_refine_e42c37ee1e9e53704204cc8662ff2f71",
        "typing_FStar.Buffer.__proj__MkBuffer__item__content",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.Buffer.__proj__MkBuffer__item__max_length",
        "typing_FStar.UInt32.v"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode",
      4,
      0,
      1,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing",
        "constructor_distinct_Prims.Mktuple2",
        "data_elim_FStar.Buffer.MkBuffer", "data_elim_FStar.HyperStack.HS",
        "data_elim_FStar.UInt32.Mk", "equation_FStar.Buffer.as_seq",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.contains",
        "equation_FStar.Buffer.idx", "equation_FStar.Buffer.includes",
        "equation_FStar.Buffer.length", "equation_FStar.Buffer.live",
        "equation_FStar.Buffer.offset", "equation_FStar.Buffer.sel",
        "equation_FStar.Buffer.sub", "equation_FStar.HyperHeap.t",
        "equation_FStar.HyperStack.hh",
        "equation_FStar.List.Tot.Base.test_sort",
        "equation_FStar.Mul.op_Star", "equation_FStar.Seq.Properties.split",
        "equation_FStar.UInt.add", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.sub",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.add",
        "equation_FStar.UInt32.n", "equation_FStar.UInt32.sub",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
        "equation_FStar.UInt32.v", "equation_FStar.UInt64.uint_to_t",
        "equation_FStar.UInt64.v", "equation_FStar.UInt8.t",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt8.t",
        "equation_Prims._assert", "equation_Prims.nat",
        "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.block",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant2",
        "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_cipher",
        "equation_Spec.Salsa20.salsa20_ctx",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_guarded_inversion_FStar.HyperStack.reference",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "function_token_typing_FStar.HyperHeap.root",
        "function_token_typing_FStar.List.Tot.Base.test_sort",
        "function_token_typing_Spec.Salsa20.constant2", "int_inversion",
        "int_typing", "kinding_FStar.UInt8.t_@tok",
        "lemma_FStar.Buffer.lemma_offset_spec",
        "lemma_FStar.Buffer.lemma_size", "lemma_FStar.Buffer.lemma_sub_spec",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "proj_equation_FStar.Buffer.MkBuffer_idx",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.Buffer.MkBuffer_max_length",
        "proj_equation_FStar.HyperStack.HS_h",
        "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Buffer.MkBuffer_content",
        "projection_inverse_FStar.Buffer.MkBuffer_idx",
        "projection_inverse_FStar.Buffer.MkBuffer_length",
        "projection_inverse_FStar.UInt32.Mk_v",
        "projection_inverse_FStar.UInt64.Mk_v",
        "projection_inverse_Prims.Mktuple2__1",
        "projection_inverse_Prims.Mktuple2__2",
        "projection_inverse_Prims.Mktuple2__a",
        "projection_inverse_Prims.Mktuple2__b",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_0991f788dbb220993dffda8c3c28b9ce",
        "refinement_interpretation_Tm_refine_0c39788a35c67ccb2b6c008a42650895",
        "refinement_interpretation_Tm_refine_0dc1829dbc3c1d1c42b7a4e9e5c89884",
        "refinement_interpretation_Tm_refine_109859f7283d820caaab3211c004ad66",
        "refinement_interpretation_Tm_refine_27eb738955e795e5dd1cab5fe18de9a0",
        "refinement_interpretation_Tm_refine_4eb09d73aa2900d334961d999d08edb6",
        "refinement_interpretation_Tm_refine_5460149187704503c8495590de3b3f5d",
        "refinement_interpretation_Tm_refine_5ec5b64a8a200c47ed44dad76f0de705",
        "refinement_interpretation_Tm_refine_641a4cf36484c6d725c0070fa6553252",
        "refinement_interpretation_Tm_refine_6dcb21a272243833262302041761c187",
        "refinement_interpretation_Tm_refine_77463d184b38c9a703782d18ac88db69",
        "refinement_interpretation_Tm_refine_7874c81428902f5ef0683ead2eab5830",
        "refinement_interpretation_Tm_refine_7e3beb6acccffb41919f80afab550fdd",
        "refinement_interpretation_Tm_refine_907182d4e2170b57b8441f948a734676",
        "refinement_interpretation_Tm_refine_98933cd3eef38f55306d74c56b536cf9",
        "refinement_interpretation_Tm_refine_a121f8bda6f05793d62ed0cfe5b942df",
        "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
        "refinement_interpretation_Tm_refine_a341af39caff669bb0afe0b53bc92beb",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c1af962245efd987b248097ce687cffa",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea",
        "refinement_interpretation_Tm_refine_dca010ec7aae3ea7c12c586af7fbfc77",
        "refinement_interpretation_Tm_refine_e42c37ee1e9e53704204cc8662ff2f71",
        "refinement_interpretation_Tm_refine_e846d5f5e465a29c0692fc9edab3f0c8",
        "refinement_interpretation_Tm_refine_ec8c52b60e5c33b3ae66e4063643ec19",
        "refinement_kinding_Tm_refine_98933cd3eef38f55306d74c56b536cf9",
        "refinement_kinding_Tm_refine_a121f8bda6f05793d62ed0cfe5b942df",
        "token_correspondence_Spec.Salsa20.salsa20_block",
        "typing_FStar.Buffer.__proj__MkBuffer__item__content",
        "typing_FStar.Buffer.__proj__MkBuffer__item__idx",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.Buffer.__proj__MkBuffer__item__max_length",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.idx",
        "typing_FStar.Buffer.length", "typing_FStar.Buffer.offset",
        "typing_FStar.Buffer.sub",
        "typing_FStar.HyperStack.__proj__HS__item__h",
        "typing_FStar.HyperStack.is_in", "typing_FStar.HyperStack.sel",
        "typing_FStar.Seq.Base.append", "typing_FStar.UInt32.v",
        "typing_Spec.Salsa20.salsa20_block", "unit_inversion"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_counter_mode_",
      1,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_counter_mode_",
      2,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_counter_mode_",
      3,
      0,
      0,
      [
        "@query", "equation_FStar.Buffer.length",
        "equation_FStar.Mul.op_Star", "equation_FStar.UInt64.n",
        "equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
        "equation_FStar.UInt8.t", "equation_Hacl.UInt8.t",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_Tm_refine_6925cb0f165c2ed09ea63ef366099574",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_counter_mode_",
      4,
      0,
      0,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.length",
        "equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.hh",
        "equation_FStar.HyperStack.is_in",
        "equation_FStar.List.Tot.Base.test_sort", "equation_FStar.UInt.eq",
        "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.eq",
        "equation_FStar.UInt32.n", "equation_FStar.UInt32.t",
        "equation_FStar.UInt32.v", "equation_FStar.UInt64.n",
        "equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
        "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.invariant",
        "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt32.t",
        "equation_Hacl.UInt8.t", "equation_Prims._assert",
        "equation_Prims.nat", "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "function_token_typing_FStar.Heap.emp",
        "function_token_typing_FStar.HyperHeap.root",
        "function_token_typing_FStar.List.Tot.Base.test_sort",
        "int_inversion", "kinding_FStar.UInt32.t_@tok",
        "kinding_FStar.UInt8.t_@tok",
        "lemma_FStar.Buffer.lemma_modifies_sub_2",
        "pretyping_6c86c071b92797cdf01eb016249a9465",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.HyperStack.HS_h",
        "proj_equation_FStar.UInt32.Mk_v",
        "proj_equation_Hacl.Impl.Salsa20.MkLog_k",
        "proj_equation_Hacl.Impl.Salsa20.MkLog_n",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_0dc1829dbc3c1d1c42b7a4e9e5c89884",
        "refinement_interpretation_Tm_refine_61b49facf2d28ca9c11c0eebf24ee9f9",
        "refinement_interpretation_Tm_refine_6925cb0f165c2ed09ea63ef366099574",
        "refinement_interpretation_Tm_refine_790772d82e6c5382184d4482620e08ca",
        "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_cdad18d4eea688c87fdef10082480b22",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Tm_refine_e7f878c767ff5e47f70ac888f769e85f",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.Buffer.length",
        "typing_FStar.HyperStack.__proj__HS__item__h",
        "typing_FStar.HyperStack.is_in", "typing_FStar.Seq.Base.createEmpty",
        "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "unit_inversion"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_counter_mode",
      1,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_counter_mode",
      2,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_counter_mode",
      3,
      0,
      0,
      [
        "@query", "equation_FStar.Buffer.length",
        "equation_FStar.Mul.op_Star", "equation_FStar.UInt64.n",
        "equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
        "equation_FStar.UInt8.t", "equation_Hacl.UInt8.t",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_Tm_refine_6925cb0f165c2ed09ea63ef366099574",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_counter_mode",
      4,
      0,
      1,
      [
        "@query", "b2t_def", "bool_inversion", "bool_typing",
        "data_elim_FStar.Buffer.MkBuffer", "data_elim_FStar.UInt32.Mk",
        "data_elim_Spec.CTR.Mkblock_cipher_ctx",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.contains",
        "equation_FStar.Buffer.disjoint", "equation_FStar.Buffer.equal",
        "equation_FStar.Buffer.idx", "equation_FStar.Buffer.includes",
        "equation_FStar.Buffer.length", "equation_FStar.Buffer.live",
        "equation_FStar.Buffer.offset", "equation_FStar.Buffer.sub",
        "equation_FStar.Ghost.reveal", "equation_FStar.HyperHeap.t",
        "equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_in",
        "equation_FStar.List.Tot.Base.test_sort",
        "equation_FStar.Mul.op_Star", "equation_FStar.UInt.add",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.lt",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.sub",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.add",
        "equation_FStar.UInt32.lt", "equation_FStar.UInt32.n",
        "equation_FStar.UInt32.sub", "equation_FStar.UInt32.t",
        "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v",
        "equation_FStar.UInt64.n", "equation_FStar.UInt64.t",
        "equation_FStar.UInt64.v", "equation_FStar.UInt8.t",
        "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.invariant",
        "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt32.t",
        "equation_Hacl.UInt8.t", "equation_Prims._assert",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant2",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "fuel_correspondence_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_guarded_inversion_FStar.HyperStack.reference",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "function_token_typing_FStar.Heap.emp",
        "function_token_typing_FStar.HyperHeap.root",
        "function_token_typing_FStar.List.Tot.Base.test_sort",
        "function_token_typing_Spec.Salsa20.constant2",
        "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_typing",
        "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok",
        "lemma_FStar.Buffer.lemma_disjoint_sub",
        "lemma_FStar.Buffer.lemma_disjoint_sub_",
        "lemma_FStar.Buffer.lemma_disjoint_symm",
        "lemma_FStar.Buffer.lemma_modifies_2_trans_",
        "lemma_FStar.Buffer.lemma_offset_spec",
        "lemma_FStar.Buffer.modifies_subbuffer_2",
        "lemma_FStar.Buffer.no_upd_lemma_2",
        "lemma_FStar.HyperStack.lemma_equal_domains_trans",
        "pretyping_6c86c071b92797cdf01eb016249a9465",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "proj_equation_FStar.Buffer.MkBuffer_idx",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.Buffer.MkBuffer_max_length",
        "proj_equation_FStar.HyperStack.HS_h",
        "proj_equation_FStar.UInt32.Mk_v",
        "proj_equation_Hacl.Impl.Salsa20.MkLog_k",
        "proj_equation_Hacl.Impl.Salsa20.MkLog_n",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Buffer.MkBuffer_idx",
        "projection_inverse_FStar.Buffer.MkBuffer_length",
        "projection_inverse_FStar.UInt32.Mk_v",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_Tm_refine_03d0bed5c0733099844f268aecd0836d",
        "refinement_interpretation_Tm_refine_0dc1829dbc3c1d1c42b7a4e9e5c89884",
        "refinement_interpretation_Tm_refine_347445ef4893546fd9bf59fd6955c377",
        "refinement_interpretation_Tm_refine_5460149187704503c8495590de3b3f5d",
        "refinement_interpretation_Tm_refine_6925cb0f165c2ed09ea63ef366099574",
        "refinement_interpretation_Tm_refine_790772d82e6c5382184d4482620e08ca",
        "refinement_interpretation_Tm_refine_907182d4e2170b57b8441f948a734676",
        "refinement_interpretation_Tm_refine_9d836f17260390394ee04e04c2340c0e",
        "refinement_interpretation_Tm_refine_a2e6366d2de5a2469cf7063420642cdc",
        "refinement_interpretation_Tm_refine_aef6ec9d3290a1c96570fbfd09471f2e",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
        "refinement_interpretation_Tm_refine_cdad18d4eea688c87fdef10082480b22",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.Buffer.__proj__MkBuffer__item__content",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.Buffer.__proj__MkBuffer__item__max_length",
        "typing_FStar.Buffer.length",
        "typing_FStar.HyperStack.__proj__HS__item__h",
        "typing_FStar.HyperStack.is_in", "typing_FStar.UInt.fits",
        "typing_FStar.UInt32.sub", "typing_FStar.UInt32.v",
        "typing_FStar.UInt64.v", "unit_inversion"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20",
      1,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20",
      2,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqTm_refine_89ca984d58100ebf87df2ad1ed88d530",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20",
      3,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20",
      4,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20",
      5,
      0,
      1,
      [
        "@query", "equation_FStar.Buffer.length",
        "equation_FStar.Mul.op_Star", "equation_FStar.UInt64.n",
        "equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
        "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p",
        "equation_Hacl.UInt8.t", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_Tm_refine_37a0857914d89104011d086c3ad059e7",
        "refinement_interpretation_Tm_refine_3bc04952e495dc70c0ea20124c41a18c",
        "refinement_interpretation_Tm_refine_6925cb0f165c2ed09ea63ef366099574",
        "refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38"
      ],
      0
    ],
    [
      "Hacl.Impl.Salsa20.salsa20",
      6,
      0,
      1,
      [
        "@query", "assumption_FStar.HyperHeap.HasEq_rid", "bool_inversion",
        "data_elim_FStar.Buffer.MkBuffer", "data_elim_FStar.HyperStack.HS",
        "data_elim_FStar.HyperStack.MkRef", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.contains", "equation_FStar.Buffer.content",
        "equation_FStar.Buffer.equal", "equation_FStar.Buffer.frameOf",
        "equation_FStar.Buffer.live",
        "equation_FStar.HyperHeap.map_invariant",
        "equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.contains",
        "equation_FStar.HyperStack.equal_domains",
        "equation_FStar.HyperStack.frameOf",
        "equation_FStar.HyperStack.fresh_frame",
        "equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_in",
        "equation_FStar.HyperStack.is_tip",
        "equation_FStar.HyperStack.live_region",
        "equation_FStar.HyperStack.pop",
        "equation_FStar.HyperStack.poppable",
        "equation_FStar.ST.inline_stack_inv", "equation_FStar.Set.eqtype",
        "equation_FStar.UInt32.t", "equation_FStar.UInt8.t",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt32.t",
        "equation_Hacl.UInt8.t",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "fuel_guarded_inversion_FStar.HyperStack.reference",
        "function_token_typing_FStar.Heap.emp",
        "function_token_typing_FStar.Heap.heap",
        "function_token_typing_FStar.HyperHeap.rid",
        "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok",
        "lemma_FStar.Buffer.lemma_disjoint_symm",
        "lemma_FStar.Buffer.lemma_equal_domains_2",
        "lemma_FStar.Buffer.lemma_fresh_poppable",
        "lemma_FStar.Buffer.lemma_live_disjoint",
        "lemma_FStar.Buffer.lemma_modifies_0_1_",
        "lemma_FStar.Buffer.lemma_modifies_0_2",
        "lemma_FStar.Buffer.lemma_modifies_2_comm",
        "lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped",
        "lemma_FStar.Buffer.modifies_poppable_2",
        "lemma_FStar.Buffer.modifies_popped_1",
        "lemma_FStar.Buffer.no_upd_fresh",
        "lemma_FStar.Buffer.no_upd_lemma_0",
        "lemma_FStar.Buffer.no_upd_lemma_1",
        "lemma_FStar.Buffer.no_upd_popped",
        "lemma_FStar.HyperStack.lemma_equal_domains_trans",
        "pretyping_6c86c071b92797cdf01eb016249a9465",
        "pretyping_730e633374418435590e5214be2471d4",
        "primitive_Prims.op_disEquality",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "proj_equation_FStar.HyperStack.HS_h",
        "proj_equation_FStar.HyperStack.HS_tip",
        "proj_equation_FStar.HyperStack.MkRef_id",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_0dc1829dbc3c1d1c42b7a4e9e5c89884",
        "refinement_interpretation_Tm_refine_37a0857914d89104011d086c3ad059e7",
        "refinement_interpretation_Tm_refine_3bc04952e495dc70c0ea20124c41a18c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_790772d82e6c5382184d4482620e08ca",
        "refinement_interpretation_Tm_refine_aef6ec9d3290a1c96570fbfd09471f2e",
        "refinement_interpretation_Tm_refine_d023b9461e4d4c2c1260f907a1d7e4a1",
        "refinement_interpretation_Tm_refine_de8123dd3e45084cdea7d9d0e7ffb100",
        "refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.Buffer.__proj__MkBuffer__item__content",
        "typing_FStar.HyperHeap.includes",
        "typing_FStar.HyperStack.__proj__HS__item__h",
        "typing_FStar.HyperStack.__proj__HS__item__tip",
        "typing_FStar.HyperStack.poppable", "typing_FStar.Map.contains"
      ],
      0
    ]
  ]
]