[
  "�y�ŋ\b�\u0011fJ{5�E��",
  [
    [
      "Hacl.Impl.Salsa20.state",
      1,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0,
      "98759c29057a1a5ca641a934afd04c7b"
    ],
    [
      "Hacl.Impl.Salsa20.op_Less_Less_Less",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "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_Hacl.Impl.Salsa20.u32",
        "equation_Prims.nat", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_c8815129b4a7e19454e6f8a062b651d7",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.UInt32.v"
      ],
      0,
      "fe1774803baa3c1f0f46100944d1a7b4"
    ],
    [
      "Hacl.Impl.Salsa20.setup",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "assumption_Prims.HasEq_int",
        "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "function_token_typing_FStar.UInt8.t",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_34c713272d4138e534ee70be89b06637",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_59174d15900b1aac0e68774108209b07",
        "typing_FStar.Buffer.as_seq"
      ],
      0,
      "ab0b0d1aeba5824f712a14385fdbd957"
    ],
    [
      "Hacl.Impl.Salsa20.setup",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "eq2-interp", "equation_FStar.Buffer.as_seq",
        "equation_FStar.Buffer.buffer", "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.lseq",
        "equation_FStar.Buffer.max_length", "equation_FStar.Buffer.sub",
        "equation_FStar.Buffer.unused_in",
        "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.HyperStack.ST.equal_domains",
        "equation_FStar.HyperStack.ST.inline_stack_inv",
        "equation_FStar.HyperStack.ST.mreference",
        "equation_FStar.HyperStack.ST.reference",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.frameOf",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.live_region",
        "equation_FStar.Monotonic.HyperStack.mreference",
        "equation_FStar.Monotonic.HyperStack.poppable",
        "equation_FStar.Monotonic.HyperStack.popped",
        "equation_FStar.Monotonic.HyperStack.remove_elt",
        "equation_FStar.Monotonic.HyperStack.unused_in",
        "equation_FStar.Set.eqtype", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt8.n",
        "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_Prims.eq2", "equation_Prims.eqtype",
        "equation_Prims.squash", "equation_Spec.Salsa20.setup",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_Prims.equals",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.Monotonic.HyperHeap.rid",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.n",
        "function_token_typing_FStar.UInt8.t",
        "haseqFStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "int_inversion", "int_typing",
        "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_1_1",
        "lemma_FStar.Buffer.lemma_sub_spec", "lemma_FStar.Buffer.live_fresh",
        "lemma_FStar.Buffer.live_popped",
        "lemma_FStar.Buffer.modifies_poppable_2_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_popped",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement",
        "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt64.uv_inv",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
        "primitive_Prims.op_Negation", "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.Monotonic.HyperStack.HS_h",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Buffer.MkBuffer_idx",
        "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75",
        "refinement_interpretation_FStar.HyperStack.ST_Tm_refine_003cbb363565c5358e7ed8a8d7dba6d4",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ff6903d111e26694749bc08df55f1ccf",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_088c08ad7049f90a1b54c5d2f0bc8269",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_34c713272d4138e534ee70be89b06637",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_59174d15900b1aac0e68774108209b07",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_bb17305494e48d3395903549cf11c3e0",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_cc072bd00679d76de8abccc5e0f6e6ec",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Prims_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_kinding_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "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.length",
        "typing_FStar.Buffer.lseq", "typing_FStar.Buffer.max_length",
        "typing_FStar.Heap.trivial_preorder", "typing_FStar.Map.contains",
        "typing_FStar.Map.domain",
        "typing_FStar.Monotonic.HyperStack.__proj__HS__item__h",
        "typing_FStar.Monotonic.HyperStack.__proj__HS__item__tip",
        "typing_FStar.Monotonic.HyperStack.__proj__MkRef__item__frame",
        "typing_FStar.Monotonic.HyperStack.contains",
        "typing_FStar.Monotonic.HyperStack.poppable",
        "typing_FStar.Monotonic.HyperStack.remove_elt",
        "typing_FStar.Set.complement", "typing_FStar.Set.singleton",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "unit_typing"
      ],
      0,
      "bb03ed7d38ef95557707f28cddb16125"
    ],
    [
      "Hacl.Impl.Salsa20.line",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.idx",
        "equation_Hacl.Impl.Salsa20.state",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "lemma_FStar.Buffer.lemma_size", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5fd76f96dd8842f1d4e9ef690b5c4ee7",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_c8815129b4a7e19454e6f8a062b651d7",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.Buffer.as_seq", "typing_FStar.UInt32.v"
      ],
      0,
      "502dd8bb83f4cf9350334f18d4d32c20"
    ],
    [
      "Hacl.Impl.Salsa20.line",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.Buffer.buffer", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.idx",
        "equation_Hacl.Impl.Salsa20.op_Less_Less_Less",
        "equation_Hacl.Impl.Salsa20.state",
        "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.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt32.n", "int_inversion",
        "interpretation_Spec.Salsa20_Tm_abs_c99d884abfcd935d4c8bcf43ad8d4dcf",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_196084bc1ad335a40df7013012fef5be",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_4b27de1c839f19290d3d8b414f450492",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5fd76f96dd8842f1d4e9ef690b5c4ee7",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "token_correspondence_Spec.Salsa20.line", "typing_FStar.UInt32.v"
      ],
      0,
      "9746042f117d06a3de06d34d55c9b1fc"
    ],
    [
      "Hacl.Impl.Salsa20.quarter_round",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.idx",
        "equation_Hacl.Impl.Salsa20.state",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "lemma_FStar.Buffer.lemma_size",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5fd76f96dd8842f1d4e9ef690b5c4ee7",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.Buffer.as_seq", "typing_FStar.UInt32.v"
      ],
      0,
      "ce3472ecd5739f7b83fbf48407f7304b"
    ],
    [
      "Hacl.Impl.Salsa20.quarter_round",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.idx",
        "equation_Hacl.Impl.Salsa20.state", "equation_Spec.Lib.op_At",
        "equation_Spec.Salsa20.quarter_round", "equation_Spec.Salsa20.state",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t", "int_inversion",
        "lemma_FStar.Buffer.lemma_modifies_1_trans",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_4b27de1c839f19290d3d8b414f450492",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5fd76f96dd8842f1d4e9ef690b5c4ee7",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "token_correspondence_Spec.Lib.op_At",
        "token_correspondence_Spec.Salsa20.line",
        "token_correspondence_Spec.Salsa20.quarter_round",
        "typing_FStar.UInt32.v"
      ],
      0,
      "44623622c804ae584fbabec3aa61ed30"
    ],
    [
      "Hacl.Impl.Salsa20.column_round",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.state",
        "function_token_typing_FStar.UInt32.t",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.Buffer.as_seq"
      ],
      0,
      "3945f951388f6e5909b88e1c0b28acec"
    ],
    [
      "Hacl.Impl.Salsa20.column_round",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.as_seq",
        "equation_FStar.Buffer.buffer", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.state", "equation_Spec.Lib.op_At",
        "equation_Spec.Salsa20.column_round", "equation_Spec.Salsa20.state",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt32.t",
        "lemma_FStar.Buffer.lemma_modifies_1_trans",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_4b27de1c839f19290d3d8b414f450492",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "token_correspondence_Spec.Lib.op_At",
        "token_correspondence_Spec.Salsa20.quarter_round"
      ],
      0,
      "6b4e03ed5f97a9578654970abdb2c44d"
    ],
    [
      "Hacl.Impl.Salsa20.row_round",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.state",
        "function_token_typing_FStar.UInt32.t",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.Buffer.as_seq"
      ],
      0,
      "84f766971fe33d3787895a09108ef208"
    ],
    [
      "Hacl.Impl.Salsa20.row_round",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.as_seq",
        "equation_FStar.Buffer.buffer", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.state", "equation_Spec.Lib.op_At",
        "equation_Spec.Salsa20.row_round", "equation_Spec.Salsa20.state",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt32.t",
        "lemma_FStar.Buffer.lemma_modifies_1_trans",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_4b27de1c839f19290d3d8b414f450492",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "token_correspondence_Spec.Lib.op_At",
        "token_correspondence_Spec.Salsa20.quarter_round"
      ],
      0,
      "7e4436f4c0418d22718f2461a49c4bdb"
    ],
    [
      "Hacl.Impl.Salsa20.double_round",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "assumption_Prims.HasEq_int",
        "function_token_typing_FStar.UInt32.t",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.Buffer.as_seq"
      ],
      0,
      "cfad2337e9fa2810a05bfbf37a98f9d8"
    ],
    [
      "Hacl.Impl.Salsa20.double_round",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "assumption_Prims.HasEq_int",
        "equation_FStar.Buffer.buffer", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Spec.Lib.op_At", "equation_Spec.Salsa20.column_round",
        "equation_Spec.Salsa20.double_round",
        "equation_Spec.Salsa20.row_round", "equation_Spec.Salsa20.state",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt32.t",
        "lemma_FStar.Buffer.lemma_modifies_1_trans",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_4b27de1c839f19290d3d8b414f450492",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "token_correspondence_Spec.Lib.op_At"
      ],
      0,
      "7c5db3f9f8e59e7c6af05cb30f6de82d"
    ],
    [
      "Hacl.Impl.Salsa20.rounds",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.state",
        "function_token_typing_FStar.UInt32.t",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.Buffer.as_seq"
      ],
      0,
      "4fee5005501c8c545b4b4fdb2c68ba5b"
    ],
    [
      "Hacl.Impl.Salsa20.rounds",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_FStar.Buffer.buffer", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Spec.Salsa20.double_round", "equation_Spec.Salsa20.rounds",
        "equation_Spec.Salsa20.state",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_Spec.Loops.repeat_spec", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_modifies_1_trans",
        "lemma_FStar.Buffer.lemma_modifies_sub_1",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_4b27de1c839f19290d3d8b414f450492",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_625f91d571af8fd02cbc7781892417d4",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_df782de28d42cc81ec07e4d442f8388e",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e24aa266fb05b74fd47b9579c5281252",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.Buffer.as_seq", "typing_FStar.UInt32.v"
      ],
      0,
      "b7ba20700b69da2c14acae10adc86b19"
    ],
    [
      "Hacl.Impl.Salsa20.sum_states",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Prims.nat", "function_token_typing_FStar.UInt32.n",
        "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd"
      ],
      0,
      "e84f85101c303686a99a3d1bdd423e61"
    ],
    [
      "Hacl.Impl.Salsa20.sum_states",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.state",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd"
      ],
      0,
      "c5217918b78d6ff2bb5483a0329a7221"
    ],
    [
      "Hacl.Impl.Salsa20.copy_state",
      1,
      0,
      1,
      [ "@query" ],
      0,
      "b3d71e2fbba06da383c93a806dcbb01a"
    ],
    [
      "Hacl.Impl.Salsa20.copy_state",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "eq2-interp",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.equal", "equation_FStar.Buffer.live",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt32.t",
        "lemma_FStar.Buffer.lemma_disjoint_symm",
        "lemma_FStar.Buffer.no_upd_lemma_1",
        "lemma_FStar.Seq.Properties.slice_length",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_72d3c6e71283179f002e1558013c4184",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
        "typing_FStar.Buffer.as_seq"
      ],
      0,
      "8354652e4e0a519b83dd843f143b819c"
    ],
    [
      "Hacl.Impl.Salsa20.log_t_",
      1,
      0,
      1,
      [
        "@query", "assumption_FStar.Seq.Base.seq__uu___haseq",
        "assumption_FStar.UInt8.t__uu___haseq", "equation_Spec.Lib.lbytes",
        "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen",
        "function_token_typing_FStar.UInt8.t",
        "haseqFStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
      ],
      0,
      "8479c1bb95e38012f3bce7fae3695cd6"
    ],
    [
      "Hacl.Impl.Salsa20.u64_of_u32s",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def",
        "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.UInt64.n",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt64.n",
        "function_token_typing_Spec.Salsa20.salsa20_ctx",
        "haseqFStar.Int.Cast_Tm_refine_b3efc639530fd2a5a3fc84fb3d494026",
        "int_inversion", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt.shift_left_value_lemma",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Int.Cast_Tm_refine_c43881637fea8b5528f4439c75737f91",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.UInt32.v",
        "typing_FStar.UInt64.v"
      ],
      0,
      "f8fd0e919dd7f9c649327004efb1b05c"
    ],
    [
      "Hacl.Impl.Salsa20.low32_of_u64",
      1,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0,
      "592de4af212c02b180f40b7a3a202309"
    ],
    [
      "Hacl.Impl.Salsa20.high32_of_u64",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def",
        "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.UInt64.n",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt64.n",
        "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion",
        "lemma_FStar.UInt.shift_right_value_lemma",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.UInt64.v"
      ],
      0,
      "743f4e9be1b1b5838b8632a8fc7b26a9"
    ],
    [
      "Hacl.Impl.Salsa20.invariant",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.state",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8"
      ],
      0,
      "e1fa127234fe3bb48b13f9898e8f1a5f"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_invariant",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "eq2-interp",
        "equation_FStar.UInt32.n", "equation_Prims.eq2",
        "equation_Prims.pos", "equation_Prims.squash",
        "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",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.t",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_87a8b71348d8fdaab777237aed4f24d5",
        "refinement_interpretation_Prims_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt64.v",
        "typing_Prims.pow2", "typing_Spec.Salsa20.setup"
      ],
      0,
      "3acd2558fa73818a0aa918b098e9144d"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_invariant",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "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_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.idx", "equation_Spec.Salsa20.key",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce",
        "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.setup",
        "equation_Spec.Salsa20.state",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Spec.Salsa20.constant0",
        "function_token_typing_Spec.Salsa20.constant1",
        "function_token_typing_Spec.Salsa20.constant2",
        "function_token_typing_Spec.Salsa20.constant3",
        "haseqFStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "int_inversion", "int_typing", "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", "lemma_FStar.UInt64.uv_inv",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5bd15344e8c82029dbd5f52e1cb2d343",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_87a8b71348d8fdaab777237aed4f24d5",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_bc6c52d29034391073f85134bfce80f4",
        "refinement_interpretation_Hacl.Spec.Endianness_Tm_refine_14dd5323a9a1a912dd915232f8c7d221",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Seq.Create_Tm_refine_03488b8732f12d7416d4f57733783c65",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
        "typing_FStar.Int.Cast.uint64_to_uint32",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_Prims.pow2", "typing_Seq.Create.create_16",
        "typing_Spec.Lib.uint32s_from_le"
      ],
      0,
      "90504deb07109e13281570c3e04ce363"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_state_counter",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Prims.pos", "equation_Spec.Lib.lbytes",
        "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.key",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.setup",
        "equation_Spec.Salsa20.state",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
        "typing_FStar.Seq.Base.length", "typing_Prims.pow2",
        "typing_Spec.Salsa20.setup"
      ],
      0,
      "0062e11da2f44470ec65ea274ecd6e24"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_state_counter",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "b2t_def", "bool_inversion", "bool_typing",
        "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.UInt64.n",
        "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.idx",
        "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",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt64.n",
        "function_token_typing_FStar.UInt8.t",
        "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", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt.shift_right_value_lemma",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
        "lemma_FStar.UInt64.vu_inv", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_FStar.UInt64_Tm_refine_a84cac4d54132da90f4dac5355f9961c",
        "refinement_interpretation_FStar.UInt64_Tm_refine_b0d613e63865150efd1f73378fdc77ae",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Seq.Create_Tm_refine_03488b8732f12d7416d4f57733783c65",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
        "typing_FStar.Int.Cast.uint64_to_uint32",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt64.shift_right",
        "typing_FStar.UInt64.uint_to_t", "typing_FStar.UInt64.v",
        "typing_Seq.Create.create_16", "typing_Spec.Lib.uint32s_from_le",
        "typing_Spec.Salsa20.setup"
      ],
      0,
      "e40c37202a03cdafc1848431e3fc2ed2"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_u64_of_u32s",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_FStar.UInt32.t__uu___haseq",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "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.UInt64.n",
        "equation_Hacl.Impl.Salsa20.high32_of_u64",
        "equation_Hacl.Impl.Salsa20.u64_of_u32s", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt64.n",
        "function_token_typing_Spec.Salsa20.salsa20_ctx",
        "haseqFStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "int_inversion", "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt.shift_right_value_lemma",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
        "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",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f",
        "refinement_interpretation_FStar.Int.Cast_Tm_refine_c43881637fea8b5528f4439c75737f91",
        "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_FStar.UInt64_Tm_refine_a84cac4d54132da90f4dac5355f9961c",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_38ba181c174bc0df2d51f0fb09d5a895",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_69d76953668d9c71d07ea76d1bc63f90",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ad73429f90f4e2d794c61307d038fc0f",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_FStar.Int.Cast.uint32_to_uint64",
        "typing_FStar.Int.Cast.uint64_to_uint32",
        "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
        "typing_FStar.UInt64.shift_right", "typing_FStar.UInt64.v",
        "typing_Hacl.Impl.Salsa20.high32_of_u64",
        "typing_Hacl.Impl.Salsa20.u64_of_u32s", "typing_Prims.pow2"
      ],
      0,
      "c287d5b1541b4f21865069badf0fb971"
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_core",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.state",
        "function_token_typing_FStar.UInt32.t",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_512d2e36eceaae5937ab1ff1eef964fd",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_7d4d53db077e83f6f072c4c682145e13",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "typing_FStar.Buffer.as_seq"
      ],
      0,
      "4eba612590724aec6c6ed0571e10bfb8"
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_core",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Hacl.Impl.Salsa20_pretyping_a87e903bbc455531fa4b8b47a243ed22",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "data_elim_Spec.CTR.Mkblock_cipher_ctx", "eq2-interp",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.equal", "equation_FStar.Buffer.get",
        "equation_FStar.Buffer.live", "equation_FStar.Buffer.lseq",
        "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.HyperStack.ST.mreference",
        "equation_FStar.HyperStack.ST.reference",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Hacl.Cast.uint32_to_sint32",
        "equation_Hacl.Cast.uint64_to_sint64",
        "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.Spec.Endianness.h32_to_u32",
        "equation_Hacl.Spec.Endianness.h64_to_u64", "equation_Prims.nat",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_core",
        "equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.setup",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_Spec.Salsa20.salsa20_ctx",
        "haseqFStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "int_typing", "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.ST.lemma_equal_domains_trans",
        "lemma_FStar.Seq.Base.lemma_index_upd1",
        "lemma_FStar.Seq.Base.lemma_index_upd2", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt64.uv_inv", "primitive_Prims.op_AmpAmp",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "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.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.HyperStack.ST_Tm_refine_003cbb363565c5358e7ed8a8d7dba6d4",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_2f9497792558fc9d93d5b47583281d2b",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_38ba181c174bc0df2d51f0fb09d5a895",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_512d2e36eceaae5937ab1ff1eef964fd",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_52d69bc24c6980fdfabfdd0c8d48390f",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_7d4d53db077e83f6f072c4c682145e13",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_kinding_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "typing_FStar.Buffer.__proj__MkBuffer__item__content",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Ghost.reveal",
        "typing_FStar.Heap.trivial_preorder",
        "typing_FStar.Monotonic.HyperStack.contains",
        "typing_Hacl.Impl.Salsa20.u64_of_u32s"
      ],
      0,
      "60cccf019b8ef49f3471bbeb04f06954"
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_block",
      1,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0,
      "b39f5aa0f6676ce89722bb07e7bcfb43"
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_block",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented",
        "@query",
        "Hacl.Impl.Salsa20_pretyping_a87e903bbc455531fa4b8b47a243ed22",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "data_elim_Hacl.Impl.Salsa20.MkLog",
        "data_elim_Spec.CTR.Mkblock_cipher_ctx", "eq2-interp",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.content", "equation_FStar.Buffer.equal",
        "equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.idx",
        "equation_FStar.Buffer.length", "equation_FStar.Buffer.live",
        "equation_FStar.Buffer.lseq", "equation_FStar.Buffer.max_length",
        "equation_FStar.Buffer.unused_in",
        "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.HyperStack.ST.equal_domains",
        "equation_FStar.HyperStack.ST.inline_stack_inv",
        "equation_FStar.HyperStack.ST.mreference",
        "equation_FStar.HyperStack.ST.reference",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.frameOf",
        "equation_FStar.Monotonic.HyperStack.fresh_frame",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.live_region",
        "equation_FStar.Monotonic.HyperStack.mreference",
        "equation_FStar.Monotonic.HyperStack.poppable",
        "equation_FStar.Monotonic.HyperStack.popped",
        "equation_FStar.Monotonic.HyperStack.remove_elt",
        "equation_FStar.Monotonic.HyperStack.unused_in",
        "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_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_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Prims.squash", "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.idx",
        "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_block",
        "equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.setup",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_",
        "fuel_guarded_inversion_Prims.equals",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.Monotonic.HyperHeap.rid",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.t",
        "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_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_3_2_comm",
        "lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped",
        "lemma_FStar.Buffer.modifies_poppable_1",
        "lemma_FStar.Buffer.modifies_poppable_2_1",
        "lemma_FStar.Buffer.no_upd_fresh",
        "lemma_FStar.Buffer.no_upd_lemma_1",
        "lemma_FStar.Buffer.no_upd_lemma_2_1",
        "lemma_FStar.Buffer.no_upd_popped", "lemma_FStar.Ghost.hide_reveal",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement",
        "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
        "lemma_FStar.UInt64.uv_inv", "primitive_Prims.op_Addition",
        "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.Monotonic.HyperStack.HS_h",
        "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.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
        "refinement_interpretation_FStar.HyperStack.ST_Tm_refine_003cbb363565c5358e7ed8a8d7dba6d4",
        "refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ff6903d111e26694749bc08df55f1ccf",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_FStar.UInt64_Tm_refine_a84cac4d54132da90f4dac5355f9961c",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_38ba181c174bc0df2d51f0fb09d5a895",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_401c6dceec5f7ff8e777e09ee5a25c1c",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5b9da90583ca5b6ff8dafcbc1c161281",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_7b8277f4aac7937ca94306760a67d045",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ad73429f90f4e2d794c61307d038fc0f",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Prims_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Seq.Create_Tm_refine_03488b8732f12d7416d4f57733783c65",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "refinement_kinding_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "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.frameOf", "typing_FStar.Buffer.idx",
        "typing_FStar.Ghost.reveal", "typing_FStar.Heap.trivial_preorder",
        "typing_FStar.Int.Cast.uint64_to_uint32",
        "typing_FStar.Map.contains", "typing_FStar.Map.domain",
        "typing_FStar.Monotonic.HyperStack.__proj__HS__item__h",
        "typing_FStar.Monotonic.HyperStack.__proj__HS__item__tip",
        "typing_FStar.Monotonic.HyperStack.__proj__MkRef__item__frame",
        "typing_FStar.Monotonic.HyperStack.live_region",
        "typing_FStar.Monotonic.HyperStack.poppable",
        "typing_FStar.Monotonic.HyperStack.remove_elt",
        "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_FStar.UInt64.v",
        "typing_Hacl.Impl.Salsa20.__proj__MkLog__item__k",
        "typing_Hacl.Impl.Salsa20.__proj__MkLog__item__n",
        "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",
        "unit_typing"
      ],
      0,
      "848b689ec1f926b11b7397cad6aba4b1"
    ],
    [
      "Hacl.Impl.Salsa20.alloc",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Buffer.unmapped_in",
        "equation_FStar.HyperStack.ST.inline_stack_inv",
        "equation_Hacl.Impl.Salsa20.h32",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem"
      ],
      0,
      "dfa0442ca4d036edee81a4e24e935a93"
    ],
    [
      "Hacl.Impl.Salsa20.init",
      1,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0,
      "8e70bc137ea4cfd73ed7d4d2e3a70950"
    ],
    [
      "Hacl.Impl.Salsa20.init",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def",
        "data_elim_Spec.CTR.Mkblock_cipher_ctx", "eq2-interp",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.equal",
        "equation_FStar.Buffer.length", "equation_FStar.Buffer.live",
        "equation_FStar.Buffer.lseq", "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.Monotonic.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_Hacl.Impl.Salsa20.h32",
        "equation_Hacl.Impl.Salsa20.invariant",
        "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_Prims.nat",
        "equation_Prims.pos", "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.idx",
        "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",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.t",
        "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", "lemma_FStar.Buffer.no_upd_lemma_1",
        "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt64.vu_inv",
        "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_content",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "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_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_FStar.UInt64_Tm_refine_a84cac4d54132da90f4dac5355f9961c",
        "refinement_interpretation_FStar.UInt64_Tm_refine_b0d613e63865150efd1f73378fdc77ae",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_34c713272d4138e534ee70be89b06637",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_38ba181c174bc0df2d51f0fb09d5a895",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_59174d15900b1aac0e68774108209b07",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_6aa1ec763d1c295e2e04032d3f087688",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_a4c77d45897f44b25f77ea93cf941da6",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_c1641f6080f5672f1a7f95e74d548486",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_f1bff5a109be7d28c81090d4cf9894b0",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Seq.Create_Tm_refine_03488b8732f12d7416d4f57733783c65",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "typing_FStar.Buffer.__proj__MkBuffer__item__length",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.Int.Cast.uint64_to_uint32",
        "typing_FStar.Seq.Base.index", "typing_FStar.UInt64.shift_right",
        "typing_FStar.UInt64.uint_to_t",
        "typing_Hacl.Impl.Salsa20.u64_of_u32s", "typing_Prims.pow2",
        "typing_Seq.Create.create_16", "typing_Spec.Lib.uint32s_from_le"
      ],
      0,
      "70f55997710c6d4e3f7e947aa49397ba"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.live",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_Hacl.Impl.Salsa20.uint8_p",
        "equation_Prims.nat", "equation_Spec.Lib.lbytes",
        "equation_Spec.Salsa20.block", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.idx",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "haseqHacl.Impl.Salsa20_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "int_inversion", "int_typing",
        "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_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_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d287bdb5105268f1b0702cd0a5b01379",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.UInt64.v", "typing_Spec.Salsa20.salsa20_block"
      ],
      0,
      "55e652385d39e3930c0213a2ce6b5f39"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Spec.CTR_interpretation_Tm_arrow_8c1eb20ec87e56ca23946ea5f24a1c2a",
        "assumption_Prims.HasEq_int", "b2t_def",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.live",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Seq.Base.op_At_Bar",
        "equation_FStar.Seq.Properties.split", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat",
        "equation_Spec.CTR.block", "equation_Spec.CTR.block_cipher",
        "equation_Spec.CTR.counter", "equation_Spec.CTR.counter_mode",
        "equation_Spec.CTR.key", "equation_Spec.CTR.nonce",
        "equation_Spec.CTR.xor", "equation_Spec.Lib.lbytes",
        "equation_Spec.Salsa20.block", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.idx",
        "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_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Spec.Salsa20.salsa20_block",
        "function_token_typing_Spec.Salsa20.salsa20_cipher",
        "haseqHacl.Impl.Salsa20_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "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_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.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_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_03127b5d59ee3055620018693b4264e8",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_446d18590a71c2142b36524fb60da559",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_a7f7d00dd3df632ad92443d8f33e2711",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d287bdb5105268f1b0702cd0a5b01379",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_fe2c5cfe46a42b35988ea97fc1a4786b",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.Seq.Base.createEmpty", "typing_FStar.Seq.Base.length",
        "typing_FStar.UInt64.v", "typing_Spec.Salsa20.salsa20_block"
      ],
      0,
      "1a1d2fc4e1643afe4db5230ffde210b9"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_2",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.idx", "equation_FStar.Buffer.length",
        "equation_FStar.Buffer.live", "equation_FStar.Buffer.lseq",
        "equation_FStar.Buffer.sel", "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.HyperStack.ST.mreference",
        "equation_FStar.HyperStack.ST.reference",
        "equation_FStar.Monotonic.HyperStack.contains",
        "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.n", "equation_Hacl.Impl.Salsa20.uint8_p",
        "equation_Prims.nat", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.idx", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "haseqHacl.Impl.Salsa20_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "int_inversion", "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "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_content",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "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.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.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_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.HyperStack.ST_Tm_refine_003cbb363565c5358e7ed8a8d7dba6d4",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_4d5f76b1705708752e4f3bb8d5a207ec",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ac03c6b5bfee50cc2664154412b8d06c",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "refinement_kinding_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "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.idx",
        "typing_FStar.Buffer.length", "typing_FStar.Buffer.sel",
        "typing_FStar.Heap.trivial_preorder",
        "typing_FStar.Monotonic.HyperStack.sel", "typing_FStar.UInt32.v",
        "typing_FStar.UInt64.v"
      ],
      0,
      "29ec563914c367f20499bc13b7e473ca"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_2",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_correspondence_Spec.CTR.counter_mode_blocks.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Spec.CTR.counter_mode_blocks.fuel_instrumented",
        "@query",
        "FStar.Ghost_interpretation_Tm_arrow_f529f4c9cbc78ef050cefd8cf570168e",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Spec.CTR_interpretation_Tm_arrow_8c1eb20ec87e56ca23946ea5f24a1c2a",
        "assumption_Prims.HasEq_int", "b2t_def",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.live",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Seq.Base.op_At_Bar", "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_Hacl.Impl.Salsa20.uint8_p",
        "equation_Spec.CTR.block", "equation_Spec.CTR.block_cipher",
        "equation_Spec.CTR.counter", "equation_Spec.CTR.key",
        "equation_Spec.CTR.nonce", "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",
        "equation_with_fuel_Spec.CTR.counter_mode_blocks.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Spec.Salsa20.salsa20_block",
        "function_token_typing_Spec.Salsa20.salsa20_cipher",
        "haseqHacl.Impl.Salsa20_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "int_inversion", "int_typing", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "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_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_4d5f76b1705708752e4f3bb8d5a207ec",
        "token_correspondence_Spec.Salsa20.salsa20_block",
        "typing_FStar.Buffer.as_seq", "typing_FStar.UInt64.v"
      ],
      0,
      "2857c3c3435ceda6719325ba08ce2ba8"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "equation_FStar.Buffer.buffer",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Spec.Salsa20.salsa20_ctx",
        "haseqHacl.Impl.Salsa20_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "int_inversion", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "primitive_Prims.op_Modulus", "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_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_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_241d61c8ad097706dd0ca2556ca9bdf1",
        "typing_FStar.Buffer.as_seq", "typing_FStar.UInt64.v",
        "typing_Spec.CTR.__proj__Mkblock_cipher_ctx__item__counterbits"
      ],
      0,
      "88535ed5ac4ced538dfc4c8cf778c9b3"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.CTR.counter_mode_blocks.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.live",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat",
        "equation_Spec.Salsa20.salsa20_cipher",
        "equation_Spec.Salsa20.salsa20_ctx",
        "equation_with_fuel_Spec.CTR.counter_mode_blocks.fuel_instrumented",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "haseqHacl.Impl.Salsa20_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "int_inversion", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_241d61c8ad097706dd0ca2556ca9bdf1",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_75fe8a65f5666eaf920693fe19efc919",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Seq.Base.createEmpty",
        "typing_FStar.UInt64.v"
      ],
      0,
      "294f10e2778f7e85d45e5a499ef8fcf7"
    ],
    [
      "Hacl.Impl.Salsa20.update_last",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Ghost_interpretation_Tm_arrow_f529f4c9cbc78ef050cefd8cf570168e",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.idx", "equation_FStar.Buffer.length",
        "equation_FStar.Buffer.live",
        "equation_FStar.Monotonic.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_Hacl.Impl.Salsa20.uint8_p", "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.idx",
        "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_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Spec.Salsa20.salsa20_block",
        "haseqHacl.Impl.Salsa20_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "int_inversion", "int_typing",
        "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_Subtraction",
        "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_BoxBool_proj_0",
        "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_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d287bdb5105268f1b0702cd0a5b01379",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "typing_FStar.Buffer.__proj__MkBuffer__item__idx",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.idx",
        "typing_FStar.Buffer.length", "typing_FStar.Seq.Base.length",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_FStar.UInt64.v"
      ],
      0,
      "f46b9b17b3fdbd14f784e7b1dca8dd05"
    ],
    [
      "Hacl.Impl.Salsa20.update_last",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Hacl.Impl.Salsa20_pretyping_a87e903bbc455531fa4b8b47a243ed22",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "data_elim_FStar.Buffer.MkBuffer", "eq2-interp",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "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.lseq",
        "equation_FStar.Buffer.max_length", "equation_FStar.Buffer.sel",
        "equation_FStar.Buffer.sub", "equation_FStar.Buffer.unused_in",
        "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.HyperStack.ST.equal_domains",
        "equation_FStar.HyperStack.ST.inline_stack_inv",
        "equation_FStar.HyperStack.ST.mreference",
        "equation_FStar.HyperStack.ST.reference",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.frameOf",
        "equation_FStar.Monotonic.HyperStack.fresh_frame",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.live_region",
        "equation_FStar.Monotonic.HyperStack.mreference",
        "equation_FStar.Monotonic.HyperStack.poppable",
        "equation_FStar.Monotonic.HyperStack.unused_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_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_Prims.eq2",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Spec.CTR.xor", "equation_Spec.Salsa20.salsa20_cipher",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference_",
        "fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_",
        "fuel_guarded_inversion_Prims.equals",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.t",
        "haseqHacl.Impl.Salsa20_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "int_inversion", "int_typing",
        "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_3_2_comm",
        "lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped",
        "lemma_FStar.Buffer.modifies_poppable_1",
        "lemma_FStar.Buffer.modifies_poppable_2_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.Ghost.hide_reveal",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
        "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_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.Buffer.MkBuffer_idx",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8518e8b728e19b2937c780d25ff7abcb",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.HyperStack.ST_Tm_refine_003cbb363565c5358e7ed8a8d7dba6d4",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ff6903d111e26694749bc08df55f1ccf",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_8022e3a3b2d5e770cff97a66413d2093",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_82db053939908f699a97088907080433",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d287bdb5105268f1b0702cd0a5b01379",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
        "refinement_interpretation_Prims_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "token_correspondence_Spec.Salsa20.salsa20_block",
        "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.idx", "typing_FStar.Buffer.length",
        "typing_FStar.Buffer.lseq", "typing_FStar.Buffer.max_length",
        "typing_FStar.Buffer.sel", "typing_FStar.Ghost.reveal",
        "typing_FStar.Heap.trivial_preorder",
        "typing_FStar.Monotonic.HyperStack.__proj__HS__item__tip",
        "typing_FStar.Monotonic.HyperStack.contains",
        "typing_FStar.Monotonic.HyperStack.sel", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "unit_typing"
      ],
      0,
      "321a52e12a542c4ff92725927ed7be7f"
    ],
    [
      "Hacl.Impl.Salsa20.update",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "assumption_Prims.HasEq_int",
        "equation_Hacl.Impl.Salsa20.uint8_p",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "function_token_typing_FStar.UInt8.t", "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_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_1d668d298fe099f2dd7e1e24c538b64a",
        "typing_FStar.Buffer.as_seq"
      ],
      0,
      "e5c06885012bb354472600fd655bfc00"
    ],
    [
      "Hacl.Impl.Salsa20.update",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented",
        "@query",
        "Hacl.Impl.Salsa20_pretyping_a87e903bbc455531fa4b8b47a243ed22",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "data_elim_Hacl.Impl.Salsa20.MkLog",
        "data_elim_Spec.CTR.Mkblock_cipher_ctx", "eq2-interp",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "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.lseq", "equation_FStar.Buffer.max_length",
        "equation_FStar.Buffer.sub", "equation_FStar.Buffer.unused_in",
        "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.HyperStack.ST.equal_domains",
        "equation_FStar.HyperStack.ST.inline_stack_inv",
        "equation_FStar.HyperStack.ST.mreference",
        "equation_FStar.HyperStack.ST.reference",
        "equation_FStar.Monotonic.Heap.equal_dom",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.frameOf",
        "equation_FStar.Monotonic.HyperStack.fresh_frame",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.live_region",
        "equation_FStar.Monotonic.HyperStack.mreference",
        "equation_FStar.Monotonic.HyperStack.pop",
        "equation_FStar.Monotonic.HyperStack.poppable",
        "equation_FStar.Monotonic.HyperStack.popped",
        "equation_FStar.Monotonic.HyperStack.remove_elt",
        "equation_FStar.Monotonic.HyperStack.unused_in",
        "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_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.Impl.Xor.Lemmas.u32",
        "equation_Hacl.Spec.Endianness.h32_to_u32", "equation_Prims.eq2",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Prims.squash", "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.idx",
        "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_block",
        "equation_Spec.Salsa20.salsa20_cipher",
        "equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.setup",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_",
        "fuel_guarded_inversion_Prims.equals",
        "function_token_typing_FStar.Monotonic.Heap.emp",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.Monotonic.HyperHeap.rid",
        "function_token_typing_FStar.Monotonic.HyperHeap.root",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.t",
        "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_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_3_2_comm",
        "lemma_FStar.Buffer.lemma_sub_spec", "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.Ghost.hide_reveal",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
        "lemma_FStar.Map.lemma_SelRestrict",
        "lemma_FStar.Map.lemma_UpdDomain",
        "lemma_FStar.Monotonic.Heap.lemma_contains_implies_used",
        "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement",
        "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
        "lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv", "lemma_FStar.UInt64.uv_inv",
        "primitive_Prims.op_Addition", "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_idx",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.Buffer.MkBuffer_max_length",
        "proj_equation_FStar.Monotonic.HyperStack.HS_h",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Buffer.MkBuffer_idx",
        "projection_inverse_FStar.Monotonic.HyperStack.HS_h",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.HyperStack.ST_Tm_refine_003cbb363565c5358e7ed8a8d7dba6d4",
        "refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ff6903d111e26694749bc08df55f1ccf",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_FStar.StrongExcludedMiddle_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
        "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt64_Tm_refine_a84cac4d54132da90f4dac5355f9961c",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_1d668d298fe099f2dd7e1e24c538b64a",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_38ba181c174bc0df2d51f0fb09d5a895",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_7b8277f4aac7937ca94306760a67d045",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_8022e3a3b2d5e770cff97a66413d2093",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_82db053939908f699a97088907080433",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_a8ef90a5f896f7a4d01753bf20490cfa",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ad73429f90f4e2d794c61307d038fc0f",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ce01e3cba2a2fbf2c025b891a51ea08e",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_f2cd1dcd38496b451dd6bddf03008183",
        "refinement_interpretation_Prims_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Seq.Create_Tm_refine_03488b8732f12d7416d4f57733783c65",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "refinement_kinding_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "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.content",
        "typing_FStar.Buffer.frameOf", "typing_FStar.Buffer.idx",
        "typing_FStar.Buffer.lseq", "typing_FStar.Buffer.max_length",
        "typing_FStar.Ghost.reveal", "typing_FStar.Heap.trivial_preorder",
        "typing_FStar.Int.Cast.uint64_to_uint32",
        "typing_FStar.Map.contains", "typing_FStar.Map.domain",
        "typing_FStar.Map.restrict", "typing_FStar.Map.sel",
        "typing_FStar.Monotonic.Heap.contains",
        "typing_FStar.Monotonic.Heap.unused_in",
        "typing_FStar.Monotonic.HyperStack.__proj__HS__item__h",
        "typing_FStar.Monotonic.HyperStack.__proj__HS__item__tip",
        "typing_FStar.Monotonic.HyperStack.__proj__MkRef__item__frame",
        "typing_FStar.Monotonic.HyperStack.as_ref",
        "typing_FStar.Monotonic.HyperStack.contains",
        "typing_FStar.Monotonic.HyperStack.live_region",
        "typing_FStar.Monotonic.HyperStack.poppable",
        "typing_FStar.Monotonic.HyperStack.remove_elt",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_FStar.Set.complement", "typing_FStar.Set.singleton",
        "typing_FStar.Set.union",
        "typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
        "typing_FStar.UInt64.shift_right", "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",
        "typing_Seq.Create.create_16", "typing_Spec.Lib.uint32s_from_le",
        "unit_typing"
      ],
      0,
      "bc2eba7a2b106a0b9420137d1f7bdce1"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_aux_modifies_2",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "eq2-interp", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.content", "equation_FStar.Buffer.equal",
        "equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.live",
        "equation_FStar.Buffer.lseq", "equation_FStar.Buffer.max_length",
        "equation_FStar.Buffer.modifies_buf_1",
        "equation_FStar.Buffer.modifies_buf_2",
        "equation_FStar.Buffer.to_set_2",
        "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.HyperStack.ST.mreference",
        "equation_FStar.HyperStack.ST.reference",
        "equation_FStar.Monotonic.Heap.modifies",
        "equation_FStar.Monotonic.Heap.modifies_t",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperHeap.modifies_just",
        "equation_FStar.Monotonic.HyperHeap.modifies_one",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.frameOf",
        "equation_FStar.Monotonic.HyperStack.modifies",
        "equation_FStar.Monotonic.HyperStack.modifies_one",
        "equation_FStar.Monotonic.HyperStack.modifies_ref",
        "equation_FStar.Monotonic.HyperStack.mreference",
        "equation_FStar.Set.eqtype", "equation_FStar.Set.subset",
        "equation_Prims.eqtype",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.Monotonic.HyperHeap.rid",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Map.lemma_InDomConcat",
        "lemma_FStar.Map.lemma_InDomRestrict",
        "lemma_FStar.Map.lemma_SelConcat1",
        "lemma_FStar.Map.lemma_SelConcat2",
        "lemma_FStar.Map.lemma_SelRestrict",
        "lemma_FStar.Map.lemma_equal_intro", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "proj_equation_FStar.Monotonic.HyperStack.HS_h",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_FStar.HyperStack.ST_Tm_refine_003cbb363565c5358e7ed8a8d7dba6d4",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_347cdcabc7e8becd6dd649804986fa75",
        "typing_FStar.Buffer.__proj__MkBuffer__item__content",
        "typing_FStar.Buffer.frameOf", "typing_FStar.Buffer.lseq",
        "typing_FStar.Buffer.max_length",
        "typing_FStar.Heap.trivial_preorder", "typing_FStar.Map.concat",
        "typing_FStar.Map.contains", "typing_FStar.Map.restrict",
        "typing_FStar.Monotonic.HyperStack.__proj__HS__item__h",
        "typing_FStar.Monotonic.HyperStack.__proj__MkRef__item__frame",
        "typing_FStar.Set.complement", "typing_FStar.Set.singleton",
        "typing_FStar.Set.union"
      ],
      0,
      "652a3c249c1db5471359cb15fc405d3b"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_def_0",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Prims.nat", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "function_token_typing_FStar.UInt32.n",
        "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "int_inversion", "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_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_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_6327bcdcb29e444a89cbcc4fdd08e098",
        "typing_FStar.UInt64.v"
      ],
      0,
      "8f443e35aac1ddb099d0bf6e66731ee0"
    ],
    [
      "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_def_0",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.CTR.counter_mode_blocks.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_Prims.nat",
        "equation_Spec.Salsa20.salsa20_cipher",
        "equation_Spec.Salsa20.salsa20_ctx",
        "equation_with_fuel_Spec.CTR.counter_mode_blocks.fuel_instrumented",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_eq_elim", "primitive_Prims.op_Equality",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_6327bcdcb29e444a89cbcc4fdd08e098",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.createEmpty", "typing_FStar.UInt64.v"
      ],
      0,
      "2727bdffaf13d03666406b897ac1da2b"
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_counter_mode_blocks",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.idx", "equation_FStar.Buffer.length",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
        "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_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_c605ad52f2c3598e8c57d9bb607e8bab",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
        "typing_FStar.Buffer.as_seq", "typing_FStar.UInt64.v"
      ],
      0,
      "feea87dcfcbd4ada9367391321fe4add"
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_counter_mode_blocks",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Ghost_interpretation_Tm_arrow_f529f4c9cbc78ef050cefd8cf570168e",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Spec.CTR_interpretation_Tm_arrow_8c1eb20ec87e56ca23946ea5f24a1c2a",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "data_elim_FStar.Buffer.MkBuffer",
        "data_elim_Hacl.Impl.Salsa20.MkLog", "eq2-interp",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "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.lseq", "equation_FStar.Buffer.max_length",
        "equation_FStar.Buffer.sel", "equation_FStar.Buffer.sub",
        "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.HyperStack.ST.mreference",
        "equation_FStar.HyperStack.ST.reference",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.mreference",
        "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.n", "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_Prims.eq2",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Spec.CTR.block", "equation_Spec.CTR.block_cipher",
        "equation_Spec.CTR.counter", "equation_Spec.CTR.key",
        "equation_Spec.CTR.nonce", "equation_Spec.CTR.xor",
        "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.block",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.counter",
        "equation_Spec.Salsa20.idx", "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_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference_",
        "fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_",
        "fuel_guarded_inversion_Prims.equals",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Spec.Salsa20.salsa20_block",
        "function_token_typing_Spec.Salsa20.salsa20_cipher",
        "function_token_typing_Spec.Salsa20.salsa20_ctx",
        "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "int_inversion", "int_typing",
        "kinding_Hacl.Impl.Salsa20.log_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_comm",
        "lemma_FStar.Buffer.lemma_modifies_sub_2",
        "lemma_FStar.Buffer.lemma_size", "lemma_FStar.Buffer.lemma_sub_spec",
        "lemma_FStar.Buffer.lemma_sub_spec_",
        "lemma_FStar.Buffer.no_upd_lemma_2",
        "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",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "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_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.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.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_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8518e8b728e19b2937c780d25ff7abcb",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75",
        "refinement_interpretation_FStar.Buffer_Tm_refine_9bfa201ea86c38505bfbda4d2a64c994",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ba56e54aa82f2631b0e7a66e112023c8",
        "refinement_interpretation_FStar.HyperStack.ST_Tm_refine_003cbb363565c5358e7ed8a8d7dba6d4",
        "refinement_interpretation_FStar.Int.Cast_Tm_refine_c43881637fea8b5528f4439c75737f91",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_03127b5d59ee3055620018693b4264e8",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_559c261b1c3777929ea329abfe70ab33",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
        "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_03b8e2da233e9469375bdd2aeea0d898",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_1939c57ed0c4d00b8a860ca6efb0065c",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_48e1d639f7bfe20139b9a08d7ef9c41f",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5690982ce2c559840a2bb26948ccca3b",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_7ef6588018260ed3205c9e2f80e9a646",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_8022e3a3b2d5e770cff97a66413d2093",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_82db053939908f699a97088907080433",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_9f568c1b7d9c8202f130827bb225e6f3",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_bb97f9421ca48a5674bdc5dc143108b3",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_c605ad52f2c3598e8c57d9bb607e8bab",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ca2c77f69acff4fca0b44c61a9e317a7",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_cea576a8a1350b16480a90b4f7f5dc8f",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d35190c17b5407ee0998c90ebc15054c",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
        "refinement_interpretation_Prims_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "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.length",
        "typing_FStar.Buffer.lseq", "typing_FStar.Buffer.max_length",
        "typing_FStar.Buffer.sub", "typing_FStar.Ghost.reveal",
        "typing_FStar.Heap.trivial_preorder",
        "typing_FStar.Int.Cast.uint32_to_uint64",
        "typing_FStar.Monotonic.HyperStack.contains",
        "typing_FStar.Seq.Base.createEmpty", "typing_FStar.Seq.Base.slice",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
        "typing_FStar.UInt64.v",
        "typing_Spec.CTR.__proj__Mkblock_cipher_ctx__item__keylen",
        "unit_typing"
      ],
      0,
      "eb9a3c4c65237b0d50b08b0d60210bb6"
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_counter_mode",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_Hacl.Impl.Salsa20.uint8_p",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "haseqHacl.Impl.Salsa20_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "int_inversion", "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_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
        "typing_FStar.Buffer.as_seq", "typing_FStar.UInt64.v"
      ],
      0,
      "7d4a6c2f58ea3237d4b3d551418e373d"
    ],
    [
      "Hacl.Impl.Salsa20.salsa20_counter_mode",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_correspondence_Spec.Loops.seq_map2.fuel_instrumented",
        "@query",
        "FStar.Ghost_interpretation_Tm_arrow_f529f4c9cbc78ef050cefd8cf570168e",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_9105589d4b48c1456d0057b53f4c3752",
        "FStar.Monotonic.HyperStack_pretyping_ed25b04ac1a3660bf4cdc8ae577888d8",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "data_elim_FStar.Buffer.MkBuffer",
        "data_elim_Hacl.Impl.Salsa20.MkLog",
        "data_elim_Spec.CTR.Mkblock_cipher_ctx", "eq2-interp",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "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.lseq", "equation_FStar.Buffer.max_length",
        "equation_FStar.Buffer.offset", "equation_FStar.Buffer.sel",
        "equation_FStar.Buffer.sub", "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.HyperStack.ST.mreference",
        "equation_FStar.HyperStack.ST.reference",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.mreference",
        "equation_FStar.Seq.Base.op_At_Bar",
        "equation_FStar.Seq.Properties.split", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.gt", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.gt",
        "equation_FStar.UInt32.n", "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_Prims.nat",
        "equation_Prims.pos", "equation_Spec.CTR.counter_mode",
        "equation_Spec.CTR.xor", "equation_Spec.Lib.lbytes",
        "equation_Spec.Salsa20.block", "equation_Spec.Salsa20.blocklen",
        "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.idx",
        "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_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference_",
        "fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Spec.Salsa20.salsa20_block",
        "function_token_typing_Spec.Salsa20.salsa20_ctx",
        "haseqHacl.Impl.Salsa20_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "int_inversion", "int_typing",
        "kinding_Hacl.Impl.Salsa20.log_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.lemma_size", "lemma_FStar.Buffer.lemma_sub_spec",
        "lemma_FStar.Buffer.lemma_sub_spec_",
        "lemma_FStar.Buffer.no_upd_lemma_2",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "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",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_FStar.UInt.shift_right_value_lemma",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "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_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.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.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_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.Buffer_Tm_refine_791b884a5d3a77c4bdaa82496ca94b68",
        "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ba56e54aa82f2631b0e7a66e112023c8",
        "refinement_interpretation_FStar.HyperStack.ST_Tm_refine_003cbb363565c5358e7ed8a8d7dba6d4",
        "refinement_interpretation_FStar.Int.Cast_Tm_refine_c43881637fea8b5528f4439c75737f91",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_03127b5d59ee3055620018693b4264e8",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_559c261b1c3777929ea329abfe70ab33",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
        "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_FStar.UInt32_Tm_refine_6c5b5bfca8736b34d6f700f752d1df10",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt8_Tm_refine_6206cb0b0b93a50ffdc1567233aaeb47",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_24c4c2bf5594dc2ccdbf9131f7691f01",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5dae6cc07deb38fb7b3b30dd54f76228",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5ecfbc3b1fb0a18cc9b570ff75576d79",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_75fe8a65f5666eaf920693fe19efc919",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_7be296ac13e03747b2adc677bea00ce5",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_8022e3a3b2d5e770cff97a66413d2093",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_82db053939908f699a97088907080433",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_9130dc2a7e0df53ee4c78094dd3dc784",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_9a6a88ab07ab24a7502f47c39f3cbb3b",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Spec.Loops_Tm_refine_16da5dd636ef303f4b4402f063fe1ef3",
        "refinement_interpretation_Spec.Loops_Tm_refine_4af88ef44277488ec061969a3d7abb20",
        "refinement_interpretation_Spec.Salsa20_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "token_correspondence_FStar.UInt8.logxor",
        "token_correspondence_Spec.Loops.seq_map2.fuel_instrumented",
        "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.lseq",
        "typing_FStar.Buffer.max_length", "typing_FStar.Buffer.sel",
        "typing_FStar.Ghost.reveal", "typing_FStar.Heap.trivial_preorder",
        "typing_FStar.Int.Cast.uint32_to_uint64",
        "typing_FStar.Monotonic.HyperStack.sel",
        "typing_FStar.Seq.Base.createEmpty", "typing_FStar.Seq.Base.slice",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.sub", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v", "typing_FStar.UInt64.v",
        "typing_FStar.UInt8.logxor", "typing_Spec.CTR.xor",
        "typing_Spec.Loops.seq_map2"
      ],
      0,
      "fe1909945e61c86de1cf557d72891d7c"
    ],
    [
      "Hacl.Impl.Salsa20.salsa20",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.idx", "equation_FStar.Buffer.length",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Hacl.Impl.Salsa20.uint8_p",
        "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
        "equation_Spec.Salsa20.noncelen",
        "equation_Spec.Salsa20.salsa20_ctx",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "haseqHacl.Impl.Salsa20_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "int_inversion", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Division",
        "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_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_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5ecfbc3b1fb0a18cc9b570ff75576d79",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_94403ae1db118a2daa8d61fa9d371d82",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_f7f92882b9facb724e48fab91677a95d",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.UInt64.v"
      ],
      0,
      "9c263f0feee8daa908ad0e72c8ec4cb5"
    ],
    [
      "Hacl.Impl.Salsa20.salsa20",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "eq2-interp", "equation_FStar.Buffer.as_seq",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.content",
        "equation_FStar.Buffer.equal", "equation_FStar.Buffer.frameOf",
        "equation_FStar.Buffer.live", "equation_FStar.Buffer.lseq",
        "equation_FStar.Buffer.max_length",
        "equation_FStar.Buffer.unmapped_in",
        "equation_FStar.Buffer.unused_in",
        "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.HyperStack.ST.equal_domains",
        "equation_FStar.HyperStack.ST.inline_stack_inv",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.frameOf",
        "equation_FStar.Monotonic.HyperStack.fresh_frame",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.live_region",
        "equation_FStar.Monotonic.HyperStack.poppable",
        "equation_FStar.Monotonic.HyperStack.unused_in",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
        "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
        "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.eq2",
        "equation_Prims.nat", "equation_Prims.squash",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_Prims.equals",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.t",
        "haseqHacl.Impl.Salsa20_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "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.live_fresh", "lemma_FStar.Buffer.live_popped",
        "lemma_FStar.Buffer.modifies_poppable_2_1",
        "lemma_FStar.Buffer.no_upd_fresh",
        "lemma_FStar.Buffer.no_upd_lemma_0",
        "lemma_FStar.Buffer.no_upd_popped",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
        "primitive_Prims.op_disEquality",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "proj_equation_FStar.Buffer.MkBuffer_max_length",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_ff6903d111e26694749bc08df55f1ccf",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5ecfbc3b1fb0a18cc9b570ff75576d79",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_94403ae1db118a2daa8d61fa9d371d82",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_df99644bbde6f04a0650fc350b008827",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
        "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_f7f92882b9facb724e48fab91677a95d",
        "refinement_interpretation_Prims_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.length",
        "typing_FStar.Monotonic.HyperStack.__proj__HS__item__tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "unit_typing"
      ],
      0,
      "a91aecabf38176b2d9d1ba476d1cc416"
    ]
  ]
]