[
  "1���сT\u001bW\u0003�#Z\u000bU",
  [
    [
      "EverCrypt.Hash.Incremental.bytes_any_hash_fits",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W31",
        "constructor_distinct_FStar.Integers.W32",
        "constructor_distinct_FStar.Integers.W63",
        "constructor_distinct_FStar.Integers.W8",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W31@tok",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W63@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equation_EverCrypt.Hash.Incremental.bytes_any_hash",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_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",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_1431b33da4c1d2104e0028c47aa83434"
      ],
      0,
      "181205155f6f184549fd07f50d4108f6"
    ],
    [
      "EverCrypt.Hash.Incremental.any_hash_t_fits",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W31",
        "constructor_distinct_FStar.Integers.W32",
        "constructor_distinct_FStar.Integers.W63",
        "constructor_distinct_FStar.Integers.W8",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W31@tok",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W63@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equation_EverCrypt.Hash.Incremental.any_hash_t",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_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",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "refinement_interpretation_Tm_refine_bbb9361d0a9731d5c29a69af24da18c7"
      ],
      0,
      "18003622ec3f0aa96c93bcc2b5f683fa"
    ],
    [
      "EverCrypt.Hash.Incremental.loc_includes_union_l_footprint_s",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "3e52c05f8544d906679d4d2cebc4510f"
    ],
    [
      "EverCrypt.Hash.Incremental.invariant",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_EverCrypt.Hash.Incremental.state",
        "equation_LowStar.Buffer.pointer",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e"
      ],
      0,
      "441f4c76c98e092f35a02f0fc5942ddc"
    ],
    [
      "EverCrypt.Hash.Incremental.update_pre",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "9bfed01aeaf286d5df5e98bd3383d7ee"
    ],
    [
      "EverCrypt.Hash.Incremental.finish_st",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "lemma_EverCrypt.Hash.Incremental.hash_fits",
        "refinement_interpretation_Tm_refine_b9688d2cc74c3f47e54760f7117117a9"
      ],
      0,
      "5dfd7d12b19853d766064c4b69c6aa27"
    ]
  ]
]