[
  "&��E��/�3����c;",
  [
    [
      "Hacl.Impl.SHA2_256.Lemmas.size_hash",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "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.UInt8.n",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word", "equation_Prims.nat",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "function_token_typing_FStar.UInt8.n",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.size_hash", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "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",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v"
      ],
      0,
      "35458eea82c4e3547514b253056adf57"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.size_block",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.Int16.n",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word", "equation_Prims.nat",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "function_token_typing_FStar.Int16.n",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "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",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v"
      ],
      0,
      "37078b2beb0cd93ba9b0d4d2b8411ce1"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.size_len_8",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word", "equation_Prims.nat",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.size_hash", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "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",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v"
      ],
      0,
      "b76ca77999270bd3734a56cda6386cc2"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.size_state",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "data_elim_FStar.UInt32.Mk", "data_elim_FStar.UInt64.Mk",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.mul",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.mul", "equation_FStar.UInt32.n",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
        "equation_FStar.UInt32.v", "equation_FStar.UInt64.n",
        "equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t",
        "equation_Hacl.Impl.SHA2_256.Lemmas.max_input_len",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_len_8",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_ws_w", "equation_Prims.nat",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w", "equation_Spec.SHA2_256.word",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.max_input_len",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_len_8",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash", "int_inversion",
        "int_typing", "kinding_FStar.UInt32.t_@tok",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.UInt32.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.UInt32.Mk_v",
        "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.uint_to_t"
      ],
      0,
      "f904eac8aa7e8f2f2571e4663197a07a"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.Int16.n",
        "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.UInt64.n",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_ws_w", "equation_Prims.nat",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w", "equation_Spec.SHA2_256.word",
        "function_token_typing_FStar.Int16.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt64.n",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_size",
        "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_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.v"
      ],
      0,
      "e52776e76e63967ca42d63775da66c68"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.Int16.n",
        "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.UInt64.n",
        "equation_FStar.UInt8.n",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_ws_w", "equation_Prims.nat",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w", "equation_Spec.SHA2_256.word",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_FStar.Int16.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt64.n",
        "function_token_typing_FStar.UInt8.n",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_size",
        "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_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.v"
      ],
      0,
      "a7b7ba6ac21af666d9e8d8909cb97788"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_aux_0",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "equation_FStar.Monotonic.HyperHeap.test0",
        "equation_FStar.UInt.add", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.mul", "equation_FStar.UInt.size",
        "equation_FStar.UInt.sub", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.add", "equation_FStar.UInt32.n",
        "equation_FStar.UInt32.sub", "equation_FStar.UInt32.t",
        "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_ws_w",
        "equation_Prims._assert", "equation_Prims.nat",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "fuel_guarded_inversion_FStar.UInt32.t_",
        "function_token_typing_FStar.Monotonic.HyperHeap.test0",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "function_token_typing_Spec.SHA2_256.size_hash", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.UInt32.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.UInt32.Mk_v",
        "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_FStar.UInt32_Tm_refine_6c5b5bfca8736b34d6f700f752d1df10",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_a80ae1799a607ddc1693269c14ae008c",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.UInt32.sub", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v"
      ],
      0,
      "a697c23ccf7940fd458cfc66ffea5776"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_aux_1",
      1,
      0,
      0,
      [
        "@query", "assumption_Prims.HasEq_int",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "5a2cfaeaeadb1fdc7bbb3a14ccd3cebe"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_aux_2",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "unit_typing"
      ],
      0,
      "1ddac3e92f21eaa068927ccc20345942"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_ws_def_0",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "assumption_FStar.UInt32.t__uu___haseq", "equation_Prims.nat",
        "equation_Spec.SHA2_256.block_w", "equation_Spec.SHA2_256.counter",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_k_w", "equation_Spec.SHA2_256.word",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_07355958e2bf14bd0701adebc5e1bebd"
      ],
      0,
      "798881fd7d342854c80ed1725e8977f2"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_ws_def_0",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.SHA2_256.ws.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Spec.Lib.op_String_Access",
        "equation_Spec.SHA2_256.counter",
        "equation_Spec.SHA2_256.size_block_w", "equation_Spec.SHA2_256.word",
        "equation_with_fuel_Spec.SHA2_256.ws.fuel_instrumented",
        "function_token_typing_FStar.Seq.Base.index",
        "primitive_Prims.op_LessThan",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "token_correspondence_Spec.Lib.op_String_Access"
      ],
      0,
      "bbe9c140d60ba5603e1218fd158a8f55"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_ws_def_1",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_FStar.UInt32.t__uu___haseq", "equation_FStar.UInt32.n",
        "equation_Prims.nat", "equation_Spec.SHA2_256.counter",
        "equation_Spec.SHA2_256.size_k_w",
        "function_token_typing_FStar.UInt32.n", "int_inversion",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_adc11cc70b0cbf3aff68641bd02ddfc9",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "0b7ac04c658adc7392f45bb09b6be706"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_ws_def_1",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.SHA2_256.ws.fuel_instrumented",
        "@fuel_irrelevance_Spec.SHA2_256.ws.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Spec.SHA2_256.counter",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_with_fuel_Spec.SHA2_256.ws.fuel_instrumented",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_adc11cc70b0cbf3aff68641bd02ddfc9"
      ],
      0,
      "2f93215d787e009705197f503b63bec6"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_blit_slices_eq",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "function_token_typing_Prims.int",
        "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "int_typing",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "47c44162fbd0086df4bd6b99f4504f88"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_blit_slices_eq",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Set.eqtype", "equation_Prims.nat",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.Monotonic.HyperHeap.rid", "int_typing",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Seq.Properties.slice_length",
        "primitive_Prims.op_LessThanOrEqual",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_347cdcabc7e8becd6dd649804986fa75",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_81d8eb4ea5458905efb3a8d37c8eecc6",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip"
      ],
      0,
      "0d65da327541b93811fa27628304d057"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_update_multi_def",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_FStar.Seq.Base.seq__uu___haseq",
        "assumption_FStar.UInt32.t__uu___haseq",
        "assumption_Prims.HasEq_int", "b2t_def",
        "equation_FStar.Seq.Properties.split", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Spec.SHA2_256.bytes", "equation_Spec.SHA2_256.hash_w",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w",
        "equation_Spec.SHA2_256.size_word", "equation_Spec.SHA2_256.word",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "haseqFStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "int_inversion", "int_typing",
        "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "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",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Spec.SHA2_256_Tm_refine_917a473678625266298701878a3ae2c0",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.v"
      ],
      0,
      "9e8dc8a70d40d3aa855a573cb2082856"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_update_multi_def",
      2,
      1,
      1,
      [
        "@query", "assumption_Prims.HasEq_int",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_word", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "a1cbf5c96b9fc59bfe38de5faa8bbdab"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_update_multi_def",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption",
        "@fuel_correspondence_Spec.SHA2_256.update_multi.fuel_instrumented",
        "@fuel_irrelevance_Spec.SHA2_256.update_multi.fuel_instrumented",
        "@query", "equation_Spec.SHA2_256.update",
        "equation_with_fuel_Spec.SHA2_256.update_multi.fuel_instrumented"
      ],
      0,
      "5f3ee0044dc2f3c9c863bef1f0697f8b"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_eq_endianness",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.Endianness.big_endian.fuel_instrumented",
        "@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.Endianness.bytes",
        "equation_FStar.Endianness.lbytes", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt32.n",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint8_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint8_p",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "haseqHacl.Impl.SHA2_256.Lemmas_Tm_refine_a32c05d74e0c23b69c1f684beb5f0d5a",
        "lemma_FStar.Endianness.lemma_big_endian_is_bounded",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_979acfaceae8b5e62d4eb98a3f6abc3c",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_f7f92882b9facb724e48fab91677a95d",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Endianness.big_endian"
      ],
      0,
      "3f8bf6732c0a415e8bba4c043420368d"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_sub_append_2",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "data_elim_FStar.Buffer.MkBuffer",
        "data_elim_FStar.Monotonic.HyperStack.MkRef",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.idx", "equation_FStar.Buffer.length",
        "equation_FStar.Buffer.lseq", "equation_FStar.Buffer.offset",
        "equation_FStar.Buffer.sel", "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.HyperStack.ST.mreference",
        "equation_FStar.HyperStack.ST.reference",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Monotonic.HyperStack.mreference",
        "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.SHA2_256.Lemmas.uint32_t",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint8_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint8_p",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference_",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.Monotonic.HyperHeap.rid",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "haseqHacl.Impl.SHA2_256.Lemmas_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "int_inversion", "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.Map.lemma_ContainsDom",
        "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_slice",
        "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "proj_equation_FStar.Buffer.MkBuffer_idx",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.Buffer.MkBuffer_max_length",
        "proj_equation_FStar.Monotonic.HyperStack.MkRef_frame",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Buffer.MkBuffer_idx",
        "refinement_interpretation_FStar.Buffer_Tm_refine_1a84e78220991a93402184b67dad5da7",
        "refinement_interpretation_FStar.Buffer_Tm_refine_791b884a5d3a77c4bdaa82496ca94b68",
        "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ba56e54aa82f2631b0e7a66e112023c8",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ead60fa393de493a6960365861c87f8e",
        "refinement_interpretation_FStar.HyperStack.ST_Tm_refine_003cbb363565c5358e7ed8a8d7dba6d4",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "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.Properties_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "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.SHA2_256.Lemmas_Tm_refine_0d822c1e35e07b007da75da85eed3196",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_60a013f47837e7f354ffa4fbf760922e",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_75fe8a65f5666eaf920693fe19efc919",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_afa097f8b72f46cf34db4922b546c4b4",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_kinding_FStar.Seq.Properties_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.__proj__MkBuffer__item__max_length",
        "typing_FStar.Buffer.idx", "typing_FStar.Buffer.length",
        "typing_FStar.Buffer.offset", "typing_FStar.Buffer.sel",
        "typing_FStar.Heap.trivial_preorder", "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Monotonic.HyperStack.sel",
        "typing_FStar.Seq.Base.append", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v"
      ],
      0,
      "1ea38d046025be0f4ae8620c3cc176a0"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_sub_append_2",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "data_elim_FStar.Buffer.MkBuffer",
        "data_elim_FStar.Monotonic.HyperStack.MkRef",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.idx", "equation_FStar.Buffer.length",
        "equation_FStar.Buffer.lseq", "equation_FStar.Buffer.offset",
        "equation_FStar.Buffer.sel", "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.HyperStack.ST.mreference",
        "equation_FStar.HyperStack.ST.reference",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Monotonic.HyperStack.mreference",
        "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_Hacl.Impl.SHA2_256.Lemmas.uint32_t",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint8_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint8_p",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference_",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.Monotonic.HyperHeap.rid",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Spec.SHA2_256.size_hash", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.Map.lemma_ContainsDom",
        "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_slice",
        "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "proj_equation_FStar.Buffer.MkBuffer_idx",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.Buffer.MkBuffer_max_length",
        "proj_equation_FStar.Monotonic.HyperStack.MkRef_frame",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Buffer.MkBuffer_idx",
        "refinement_interpretation_FStar.Buffer_Tm_refine_1a84e78220991a93402184b67dad5da7",
        "refinement_interpretation_FStar.Buffer_Tm_refine_791b884a5d3a77c4bdaa82496ca94b68",
        "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ba56e54aa82f2631b0e7a66e112023c8",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ead60fa393de493a6960365861c87f8e",
        "refinement_interpretation_FStar.HyperStack.ST_Tm_refine_003cbb363565c5358e7ed8a8d7dba6d4",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "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.Properties_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "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.SHA2_256.Lemmas_Tm_refine_0d822c1e35e07b007da75da85eed3196",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_60a013f47837e7f354ffa4fbf760922e",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_75fe8a65f5666eaf920693fe19efc919",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_afa097f8b72f46cf34db4922b546c4b4",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "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.idx", "typing_FStar.Buffer.length",
        "typing_FStar.Buffer.offset", "typing_FStar.Buffer.sel",
        "typing_FStar.Heap.trivial_preorder", "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Monotonic.HyperStack.sel",
        "typing_FStar.Seq.Base.append", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v"
      ],
      0,
      "97e0d0c8653e496e4752ad07e9f5c715"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_sub_append_3",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "data_elim_FStar.Buffer.MkBuffer",
        "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.length",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "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.SHA2_256.Lemmas.uint32_t",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint8_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint8_p",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.Monotonic.HyperHeap.rid",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "haseqHacl.Impl.SHA2_256.Lemmas_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
        "int_inversion", "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Buffer.MkBuffer_idx",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.Buffer.MkBuffer_max_length",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_791b884a5d3a77c4bdaa82496ca94b68",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ba56e54aa82f2631b0e7a66e112023c8",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "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.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_0d822c1e35e07b007da75da85eed3196",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_60a013f47837e7f354ffa4fbf760922e",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_75fe8a65f5666eaf920693fe19efc919",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_afa097f8b72f46cf34db4922b546c4b4",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.__proj__MkBuffer__item__max_length",
        "typing_FStar.Buffer.length", "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Seq.Base.append", "typing_FStar.UInt32.v"
      ],
      0,
      "8ae831a0729b6fe61525233931f56b1e"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_sub_append_3",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "data_elim_FStar.Buffer.MkBuffer",
        "data_elim_FStar.Monotonic.HyperStack.MkRef",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.idx", "equation_FStar.Buffer.length",
        "equation_FStar.Buffer.lseq", "equation_FStar.Buffer.offset",
        "equation_FStar.Buffer.sel", "equation_FStar.Heap.trivial_preorder",
        "equation_FStar.HyperStack.ST.mreference",
        "equation_FStar.HyperStack.ST.reference",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Monotonic.HyperStack.mreference",
        "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_Hacl.Impl.SHA2_256.Lemmas.uint32_t",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint8_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint8_p",
        "equation_Prims.eqtype", "equation_Prims.nat",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference_",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.Monotonic.HyperHeap.rid",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Spec.SHA2_256.size_hash", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.Map.lemma_ContainsDom",
        "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_slice",
        "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_FStar.Buffer.MkBuffer_content",
        "proj_equation_FStar.Buffer.MkBuffer_idx",
        "proj_equation_FStar.Buffer.MkBuffer_length",
        "proj_equation_FStar.Buffer.MkBuffer_max_length",
        "proj_equation_FStar.Monotonic.HyperStack.MkRef_frame",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Buffer.MkBuffer_idx",
        "refinement_interpretation_FStar.Buffer_Tm_refine_1a84e78220991a93402184b67dad5da7",
        "refinement_interpretation_FStar.Buffer_Tm_refine_791b884a5d3a77c4bdaa82496ca94b68",
        "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ba56e54aa82f2631b0e7a66e112023c8",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ead60fa393de493a6960365861c87f8e",
        "refinement_interpretation_FStar.HyperStack.ST_Tm_refine_003cbb363565c5358e7ed8a8d7dba6d4",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "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.Properties_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "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.SHA2_256.Lemmas_Tm_refine_0d822c1e35e07b007da75da85eed3196",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_60a013f47837e7f354ffa4fbf760922e",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_75fe8a65f5666eaf920693fe19efc919",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_afa097f8b72f46cf34db4922b546c4b4",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "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.idx", "typing_FStar.Buffer.length",
        "typing_FStar.Buffer.offset", "typing_FStar.Buffer.sel",
        "typing_FStar.Heap.trivial_preorder", "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Monotonic.HyperStack.sel",
        "typing_FStar.Seq.Base.append", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v"
      ],
      0,
      "977f13c006db6c9b4efc091955cbff6a"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_pad_aux_seq",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.Endianness.bytes",
        "equation_FStar.Endianness.lbytes", "equation_FStar.Int16.n",
        "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.UInt128.n",
        "equation_Hacl.Impl.SHA2_256.Lemmas.max_input_len",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_len_8",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_t",
        "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.SHA2_256.h_0", "equation_Spec.SHA2_256.hash_w",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.max_input_len_8",
        "equation_Spec.SHA2_256.pad", "equation_Spec.SHA2_256.pad0_length",
        "equation_Spec.SHA2_256.pow2_61",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w",
        "equation_Spec.SHA2_256.size_len_8",
        "equation_Spec.SHA2_256.size_len_ul_8",
        "equation_Spec.SHA2_256.size_word", "equation_Spec.SHA2_256.word",
        "function_token_typing_FStar.Int16.n",
        "function_token_typing_FStar.UInt128.n",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.t",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.max_input_len",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_len_8",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.h_0",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.max_input_len_8",
        "function_token_typing_Spec.SHA2_256.pow2_61",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "function_token_typing_Spec.SHA2_256.size_word", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "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_len_append",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv", "lemma_FStar.UInt64.vu_inv",
        "primitive_Prims.op_Addition", "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.Endianness_Tm_refine_1e62df159c33fd3091667f8254d1ab80",
        "refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
        "refinement_interpretation_FStar.Endianness_Tm_refine_d572874b93fe0df3a5c665d151671857",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_03127b5d59ee3055620018693b4264e8",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt8_Tm_refine_22871ed0ff70fd094ad3e8d742624d47",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_383540a0499cfe2dab7ace5acae4a9b7",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_931e65e7128473c2d4740e3590152484",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Spec.SHA2_256_Tm_refine_7e10d6c36b18f81a912b18a391ae2a16",
        "refinement_interpretation_Spec.SHA2_256_Tm_refine_b49ddfaf636afcf06cef07d1e12ced40",
        "typing_FStar.Endianness.big_bytes", "typing_FStar.Seq.Base.append",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v", "typing_FStar.UInt64.v",
        "typing_FStar.UInt8.uint_to_t", "typing_Prims.pow2",
        "typing_Spec.SHA2_256.pad0_length"
      ],
      0,
      "a5e6edca003fc24330ddf8c4fa56441c"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_pad_aux",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.Int16.n",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "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_Hacl.Impl.SHA2_256.Lemmas.max_input_len",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_len_8",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_t",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint8_ht", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.SHA2_256.k",
        "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.max_input_len_8",
        "equation_Spec.SHA2_256.pow2_61",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w",
        "equation_Spec.SHA2_256.size_word", "equation_Spec.SHA2_256.word",
        "function_token_typing_FStar.Int16.n",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.Monotonic.HyperHeap.rid",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.max_input_len",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.max_input_len_8",
        "function_token_typing_Spec.SHA2_256.pow2_61",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "function_token_typing_Spec.SHA2_256.size_word", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt.pow2_values",
        "lemma_FStar.UInt32.vu_inv", "lemma_FStar.UInt64.vu_inv",
        "primitive_Prims.op_Addition", "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.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_383540a0499cfe2dab7ace5acae4a9b7",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Spec.SHA2_256_Tm_refine_b49ddfaf636afcf06cef07d1e12ced40",
        "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v", "typing_FStar.UInt64.v"
      ],
      0,
      "a77dcd864f296fefbdf976d6d73f7240"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_spec_ws_def",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "assumption_Prims.HasEq_int",
        "equation_Prims.nat", "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_k_w", "equation_Spec.SHA2_256.word",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_07355958e2bf14bd0701adebc5e1bebd"
      ],
      0,
      "ae852e7328c01ce3a4f388e7a8331b63"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_spec_ws_def",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.SHA2_256.ws.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Spec.Lib.op_String_Access",
        "equation_Spec.SHA2_256.size_block_w", "equation_Spec.SHA2_256.word",
        "equation_with_fuel_Spec.SHA2_256.ws.fuel_instrumented",
        "function_token_typing_FStar.Seq.Base.index",
        "primitive_Prims.op_LessThan",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_07355958e2bf14bd0701adebc5e1bebd",
        "token_correspondence_Spec.Lib.op_String_Access"
      ],
      0,
      "aef126cfb01ca38fa43eddce3b318bf8"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_spec_ws_def2",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "equation_Prims.nat", "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_k_w", "equation_Spec.SHA2_256.word",
        "function_token_typing_FStar.UInt32.n", "int_inversion",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_adc11cc70b0cbf3aff68641bd02ddfc9",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "144768dda3ac03529f63c364f3325d0d"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_spec_ws_def2",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Spec.SHA2_256.ws.fuel_instrumented",
        "@fuel_irrelevance_Spec.SHA2_256.ws.fuel_instrumented", "@query",
        "assumption_Prims.HasEq_int", "equation_Prims.nat",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_with_fuel_Spec.SHA2_256.ws.fuel_instrumented",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_adc11cc70b0cbf3aff68641bd02ddfc9"
      ],
      0,
      "9f734ebc8f7562f61c9c77d68f2b814a"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_eq_state_k_sub_slice",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "equation_FStar.Buffer.buffer",
        "equation_FStar.Int16.n", "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Set.eqtype", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt8.n",
        "equation_Hacl.Hash.Lib.Create.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_ws_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_p", "equation_Prims.nat",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w",
        "equation_Spec.SHA2_256.size_len_ul_8",
        "equation_Spec.SHA2_256.word",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.Int16.n",
        "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_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "function_token_typing_Spec.SHA2_256.size_len_ul_8",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
        "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_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_dc4168d3212d5c4dd6e659d8aa600da3",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.v"
      ],
      0,
      "8d8f4abe10838885c253a452d461a022"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_eq_state_k_sub_slice",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.live", "equation_FStar.Int16.n",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Set.eqtype", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt8.n",
        "equation_Hacl.Hash.Lib.Create.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_ws_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_p", "equation_Prims.nat",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w",
        "equation_Spec.SHA2_256.size_len_ul_8",
        "equation_Spec.SHA2_256.word",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.Int16.n",
        "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_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "function_token_typing_Spec.SHA2_256.size_len_ul_8",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "int_inversion", "int_typing", "lemma_FStar.Buffer.lemma_sub_spec",
        "lemma_FStar.Map.lemma_ContainsDom", "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_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_dc4168d3212d5c4dd6e659d8aa600da3",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.v"
      ],
      0,
      "807d6e129aaf31fc47c317102df5e70a"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_eq_state_k_sub_slice",
      3,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.live", "equation_FStar.Int16.n",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "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.UInt8.n", "equation_Hacl.Hash.Lib.Create.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_ws_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_p", "equation_Prims.nat",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w",
        "equation_Spec.SHA2_256.size_len_ul_8",
        "equation_Spec.SHA2_256.word",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.Int16.n",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.Monotonic.HyperHeap.rid",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.n",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "function_token_typing_Spec.SHA2_256.size_len_ul_8", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_sub_spec",
        "lemma_FStar.Map.lemma_ContainsDom", "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_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_dc4168d3212d5c4dd6e659d8aa600da3",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.v"
      ],
      0,
      "1071aa88ee38a90f323b433968456f4f"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_eq_state_counter_sub_slice",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "equation_FStar.Buffer.buffer",
        "equation_FStar.Int16.n", "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Set.eqtype", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt8.n",
        "equation_Hacl.Hash.Lib.Create.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_ws_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_p", "equation_Prims.nat",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w",
        "equation_Spec.SHA2_256.size_len_ul_8",
        "equation_Spec.SHA2_256.word",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.Int16.n",
        "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_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "function_token_typing_Spec.SHA2_256.size_len_ul_8",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "int_inversion", "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.Map.lemma_ContainsDom", "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_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8518e8b728e19b2937c780d25ff7abcb",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_dc4168d3212d5c4dd6e659d8aa600da3",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.v"
      ],
      0,
      "2b4ff204fa52793d7e70057f707dd73d"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_eq_state_counter_sub_slice",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.live", "equation_FStar.Int16.n",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Set.eqtype", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt8.n",
        "equation_Hacl.Hash.Lib.Create.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_ws_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_p", "equation_Prims.nat",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w",
        "equation_Spec.SHA2_256.size_len_ul_8",
        "equation_Spec.SHA2_256.word",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.Int16.n",
        "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_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "function_token_typing_Spec.SHA2_256.size_len_ul_8",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "int_inversion", "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.Buffer.lemma_sub_spec",
        "lemma_FStar.Map.lemma_ContainsDom", "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_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8518e8b728e19b2937c780d25ff7abcb",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_dc4168d3212d5c4dd6e659d8aa600da3",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.v"
      ],
      0,
      "a496362b45d2bd6db85e2e6e645495ce"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_eq_state_counter_sub_slice",
      3,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.live", "equation_FStar.Int16.n",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "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.UInt8.n", "equation_Hacl.Hash.Lib.Create.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_ws_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_p", "equation_Prims.nat",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w",
        "equation_Spec.SHA2_256.size_len_ul_8",
        "equation_Spec.SHA2_256.word",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.Int16.n",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.Monotonic.HyperHeap.rid",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.n",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "function_token_typing_Spec.SHA2_256.size_len_ul_8", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_size",
        "lemma_FStar.Buffer.lemma_sub_spec",
        "lemma_FStar.Map.lemma_ContainsDom", "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_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8518e8b728e19b2937c780d25ff7abcb",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_dc4168d3212d5c4dd6e659d8aa600da3",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.v"
      ],
      0,
      "06b08d05f7fda747f0f987587d5f25d6"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_eq_state_hash_sub_slice",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "equation_FStar.Buffer.buffer",
        "equation_FStar.Int16.n", "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Set.eqtype", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt8.n",
        "equation_Hacl.Hash.Lib.Create.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_ws_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_p", "equation_Prims.nat",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w",
        "equation_Spec.SHA2_256.size_len_ul_8",
        "equation_Spec.SHA2_256.word",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.Int16.n",
        "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_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "function_token_typing_Spec.SHA2_256.size_len_ul_8",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
        "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_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_dc4168d3212d5c4dd6e659d8aa600da3",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.v"
      ],
      0,
      "7869f711962a475bc367959f1a932a08"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_eq_state_hash_sub_slice",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Prims.HasEq_int", "b2t_def", "bool_inversion",
        "bool_typing", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.live", "equation_FStar.Int16.n",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.Set.eqtype", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.n", "equation_FStar.UInt8.n",
        "equation_Hacl.Hash.Lib.Create.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_ws_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_p", "equation_Prims.nat",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w",
        "equation_Spec.SHA2_256.size_len_ul_8",
        "equation_Spec.SHA2_256.word",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.Int16.n",
        "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_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "function_token_typing_Spec.SHA2_256.size_len_ul_8",
        "haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
        "int_inversion", "int_typing", "lemma_FStar.Buffer.lemma_sub_spec",
        "lemma_FStar.Map.lemma_ContainsDom", "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_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_dc4168d3212d5c4dd6e659d8aa600da3",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.v"
      ],
      0,
      "2f6721334e919b534c6f43bc694f986f"
    ],
    [
      "Hacl.Impl.SHA2_256.Lemmas.lemma_eq_state_hash_sub_slice",
      3,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.live", "equation_FStar.Int16.n",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.contains",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "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.UInt8.n", "equation_Hacl.Hash.Lib.Create.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_whash_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Impl.SHA2_256.Lemmas.size_ws_w",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_ht",
        "equation_Hacl.Impl.SHA2_256.Lemmas.uint32_p", "equation_Prims.nat",
        "equation_Spec.SHA2_256.k", "equation_Spec.SHA2_256.k_w",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_k_w",
        "equation_Spec.SHA2_256.size_len_ul_8",
        "equation_Spec.SHA2_256.word",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "function_token_typing_FStar.Int16.n",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_FStar.Monotonic.HyperHeap.rid",
        "function_token_typing_FStar.UInt32.t",
        "function_token_typing_FStar.UInt8.n",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.pos_whash_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_block_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_count_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_k_w",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_state",
        "function_token_typing_Hacl.Impl.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.k",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "function_token_typing_Spec.SHA2_256.size_len_ul_8", "int_inversion",
        "int_typing", "lemma_FStar.Buffer.lemma_sub_spec",
        "lemma_FStar.Map.lemma_ContainsDom", "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_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_FStar.Seq.Properties_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Hacl.Impl.SHA2_256.Lemmas_Tm_refine_dc4168d3212d5c4dd6e659d8aa600da3",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
        "typing_FStar.Map.contains",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.mul", "typing_FStar.UInt32.v"
      ],
      0,
      "568c42725cf604ead71fe028a579cb25"
    ]
  ]
]