[
  "�ew�b���\u0014a0��",
  [
    [
      "Hacl.Hash.Definitions.word",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Hash.Definitions.MD5",
        "disc_equation_Spec.Hash.Definitions.SHA1",
        "disc_equation_Spec.Hash.Definitions.SHA2_224",
        "disc_equation_Spec.Hash.Definitions.SHA2_256",
        "disc_equation_Spec.Hash.Definitions.SHA2_384",
        "disc_equation_Spec.Hash.Definitions.SHA2_512",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg"
      ],
      0,
      "002dd2f9b6cf12747ff7d05d91782f3f"
    ],
    [
      "Hacl.Hash.Definitions.word_len",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Hash.Definitions.MD5",
        "disc_equation_Spec.Hash.Definitions.SHA1",
        "disc_equation_Spec.Hash.Definitions.SHA2_224",
        "disc_equation_Spec.Hash.Definitions.SHA2_256",
        "disc_equation_Spec.Hash.Definitions.SHA2_384",
        "disc_equation_Spec.Hash.Definitions.SHA2_512",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "651b89230be008e989834affdc1181f6"
    ],
    [
      "Hacl.Hash.Definitions.block_len",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "disc_equation_Spec.Hash.Definitions.MD5",
        "disc_equation_Spec.Hash.Definitions.SHA1",
        "disc_equation_Spec.Hash.Definitions.SHA2_224",
        "disc_equation_Spec.Hash.Definitions.SHA2_256",
        "disc_equation_Spec.Hash.Definitions.SHA2_384",
        "disc_equation_Spec.Hash.Definitions.SHA2_512",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "int_inversion", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "typing_Spec.Hash.Definitions.block_length"
      ],
      0,
      "175141107206ed29aa4b766f4aa6b0c3"
    ],
    [
      "Hacl.Hash.Definitions.hash_word_len",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "disc_equation_Spec.Hash.Definitions.MD5",
        "disc_equation_Spec.Hash.Definitions.SHA1",
        "disc_equation_Spec.Hash.Definitions.SHA2_224",
        "disc_equation_Spec.Hash.Definitions.SHA2_256",
        "disc_equation_Spec.Hash.Definitions.SHA2_384",
        "disc_equation_Spec.Hash.Definitions.SHA2_512",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "85ba21ebb3d0bde621aef06c9b70386d"
    ],
    [
      "Hacl.Hash.Definitions.hash_len",
      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", "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "disc_equation_Spec.Hash.Definitions.MD5",
        "disc_equation_Spec.Hash.Definitions.SHA1",
        "disc_equation_Spec.Hash.Definitions.SHA2_224",
        "disc_equation_Spec.Hash.Definitions.SHA2_256",
        "disc_equation_Spec.Hash.Definitions.SHA2_384",
        "disc_equation_Spec.Hash.Definitions.SHA2_512",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt32.n", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "function_token_typing_FStar.UInt32.n",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
        "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_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.UInt.fits", "typing_Spec.Hash.Definitions.hash_length"
      ],
      0,
      "9196c4b37d244377913c7db6dd7ac816"
    ],
    [
      "Hacl.Hash.Definitions.blocks_t",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "fa7a592ef4c95c1267c8a044b75c1f11"
    ],
    [
      "Hacl.Hash.Definitions.update_st",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Hash.Definitions.state",
        "equation_Hacl.Hash.Definitions.word",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_Spec.Hash.Definitions.word",
        "function_token_typing_FStar.UInt8.t",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "refinement_interpretation_Hacl.Hash.Definitions_Tm_refine_7fc14a39dcb3f7c36f925b07d6b8d892",
        "refinement_interpretation_Hacl.Hash.Definitions_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
        "typing_Hacl.Hash.Definitions.word",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "e60aa17ee1b43fe716297f6ac68672f9"
    ],
    [
      "Hacl.Hash.Definitions.pad_st",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.Monotonic.HyperStack.mem", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.int",
        "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Hacl.Hash.Definitions_Tm_refine_6c3118c1ad3db6b4d843c40fbd3fe4e8",
        "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "2c1cd73c3933b6fde318899b8f931892"
    ],
    [
      "Hacl.Hash.Definitions.update_multi_st",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Hash.Definitions.blocks_t",
        "equation_Hacl.Hash.Definitions.state",
        "equation_Hacl.Hash.Definitions.word",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_Spec.Hash.Definitions.word",
        "function_token_typing_FStar.UInt8.t",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "refinement_interpretation_Hacl.Hash.Definitions_Tm_refine_b041622566c63972e1ac14219bbd2812",
        "refinement_interpretation_Hacl.Hash.Definitions_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
        "typing_Hacl.Hash.Definitions.word",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "860605a6fc37a7db2ff52df10555accf"
    ],
    [
      "Hacl.Hash.Definitions.update_last_st",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equation_Hacl.Hash.Definitions.state",
        "equation_Hacl.Hash.Definitions.word",
        "equation_LowStar.Buffer.buffer",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "function_token_typing_FStar.UInt8.t",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Hacl.Hash.Definitions_Tm_refine_bccf5300d87982e3ce0f7618196189a3",
        "refinement_interpretation_Hacl.Hash.Definitions_Tm_refine_de664c97983134963ae091a4bc5e2d48",
        "refinement_interpretation_Hacl.Hash.Definitions_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
        "typing_Hacl.Hash.Definitions.word",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "6d0f38391a386b7a824ed2aa336ad98c"
    ],
    [
      "Hacl.Hash.Definitions.finish_st",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Hash.Definitions.state",
        "equation_Hacl.Hash.Definitions.word",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_Spec.Hash.Definitions.word",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "refinement_interpretation_Hacl.Hash.Definitions_Tm_refine_fed50a547a75edc3bf0cdf8183f7ebd9",
        "typing_Hacl.Hash.Definitions.word",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_Spec.Hash.Definitions.word"
      ],
      0,
      "7414f7ae183776c30d3e71439a0ed787"
    ],
    [
      "Hacl.Hash.Definitions.hash_st",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_LowStar.Buffer.buffer",
        "function_token_typing_FStar.UInt8.t",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "refinement_interpretation_Hacl.Hash.Definitions_Tm_refine_6976d4a67943951ce42b49d68f2d4fc4",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "e106d262f88337992aa0a0c793bc8bd5"
    ]
  ]
]