[
  "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.W32",
        "constructor_distinct_FStar.Integers.W64",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W64@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_898a63c05b6cf18e4d31dfeaa233fa0b"
      ],
      0,
      "708fafdaf91a5b375dd699d52bbca1dc"
    ],
    [
      "EverCrypt.Hash.Incremental.any_hash_t_fits",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W32",
        "constructor_distinct_FStar.Integers.W64",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W64@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_c3946e882ea3726bb38cf802601a8a96"
      ],
      0,
      "50b6501a0041983bef77d4382d6585e7"
    ],
    [
      "EverCrypt.Hash.Incremental.loc_includes_union_l_footprint_s",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "9bc16d61cd2916055fa611a42420ea25"
    ],
    [
      "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,
      "3df3d90763c713f5edd43055048cb6bd"
    ],
    [
      "EverCrypt.Hash.Incremental.update_pre",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "42953ad1ef35240114b47c769d7ab74a"
    ],
    [
      "EverCrypt.Hash.Incremental.finish_st",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "lemma_EverCrypt.Hash.Incremental.hash_fits",
        "refinement_interpretation_Tm_refine_b9688d2cc74c3f47e54760f7117117a9"
      ],
      0,
      "9309088674de0ebd6996602037299d2f"
    ]
  ]
]