[
  "�wB\"�\u001c� \u001e�H���2�",
  [
    [
      "EverCrypt.Hash.broken_alg",
      1,
      0,
      0,
      [ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ],
      0,
      "b7eea65bb81fd4bb17a8122445daac13"
    ],
    [
      "EverCrypt.Hash.alg13",
      1,
      0,
      0,
      [ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ],
      0,
      "f691e6bf8f0cd72ba1cff57555def793"
    ],
    [
      "EverCrypt.Hash.uint32_fits_maxLength",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "constructor_distinct_Tm_unit",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Prims.pos",
        "equation_Spec.Hash.Definitions.max_input_length", "int_inversion",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt32.v",
        "typing_Spec.Hash.Definitions.max_input_length"
      ],
      0,
      "0abb449ac2909d487b3b0115db7f40e8"
    ],
    [
      "EverCrypt.Hash.loc_includes_union_l_footprint_s",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "76e36fb280331fdc5b005fdf27a03b82"
    ],
    [
      "EverCrypt.Hash.invariant",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_EverCrypt.Hash.state",
        "equation_LowStar.Buffer.pointer",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e"
      ],
      0,
      "9f8b6ad54c7a59da3358697e112b0c45"
    ],
    [
      "EverCrypt.Hash.frame_invariant_implies_footprint_preservation",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
        "equation_EverCrypt.Hash.footprint",
        "equation_EverCrypt.Hash.invariant", "equation_EverCrypt.Hash.state",
        "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_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.get", "equation_Prims.eqtype",
        "equation_Prims.nat",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Prims.int",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
        "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
        "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
        "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
        "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_EverCrypt.Hash.footprint_s", "typing_EverCrypt.Hash.state_s",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.Set.singleton",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.as_addr",
        "typing_LowStar.Monotonic.Buffer.frameOf",
        "typing_LowStar.Monotonic.Buffer.get",
        "typing_LowStar.Monotonic.Buffer.loc_addresses",
        "typing_LowStar.Monotonic.Buffer.loc_buffer"
      ],
      0,
      "2e60a156b4c9828d1e60f5f5ccc4e79a"
    ],
    [
      "EverCrypt.Hash.update",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint8",
        "equation_LowStar.Buffer.buffer",
        "function_token_typing_Lib.IntTypes.uint8",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "refinement_interpretation_Tm_refine_ee5e5ea36a8ac8879a333964d971b753",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "1ab9edba66d85ca229bb2542b402c4d3"
    ],
    [
      "EverCrypt.Hash.update_multi",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
        "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer",
        "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_83e1a0ed8e967940f825c40ec86a30c4",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_Spec.Hash.Definitions.word_length"
      ],
      0,
      "249ed23565260ffb8b7d0c664749c576"
    ],
    [
      "EverCrypt.Hash.update_last",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def",
        "equation_EverCrypt.Helpers.uint64_t", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.uint8",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.bytes",
        "function_token_typing_Lib.IntTypes.uint8", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ca524e8b1a445d963e32596f1b3827cf",
        "refinement_interpretation_Tm_refine_cb6956610e36c497712e91628f3f016e",
        "refinement_interpretation_Tm_refine_ce8961826e5e909d22aad978d7822e9d",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt64.v", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.length"
      ],
      0,
      "6e10b66dafaf98a1403d6a6a12e4e429"
    ],
    [
      "EverCrypt.Hash.finish",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok",
        "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_Lib.IntTypes.unsigned",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "lemma_FStar.Map.lemma_ContainsDom",
        "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip"
      ],
      0,
      "e8f403a6e666d89ed9d46ab3fbd172f7"
    ],
    [
      "EverCrypt.Hash.hash",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_FStar.Monotonic.HyperStack.live_region",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "function_token_typing_Lib.IntTypes.uint8",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "lemma_LowStar.Monotonic.Buffer.live_region_frameOf",
        "refinement_interpretation_Tm_refine_117a03ca3213deec9a5d7dc6b56bb4c1",
        "refinement_interpretation_Tm_refine_11f5c63c78caccafb41a6490396f36ec",
        "refinement_interpretation_Tm_refine_70a01283c9094ee10f0f0fa4ff6403d7",
        "typing_FStar.Monotonic.HyperStack.live_region",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.frameOf"
      ],
      0,
      "652e044a6f9e4d1fd039b6490e22db6e"
    ]
  ]
]