[
  "�b#�Լݴ�!����8",
  [
    [
      "Spec.Hash.Definitions.to_blake_alg",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "equation_Spec.Hash.Definitions.blake_alg",
        "equation_Spec.Hash.Definitions.is_blake",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe"
      ],
      0,
      "429465ec52be85bf55f8955d1abe4b50"
    ],
    [
      "Spec.Hash.Definitions.to_hash_alg",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Blake2.Blake2B",
        "disc_equation_Spec.Blake2.Blake2S",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "c4c4bf9df6f9116025526ca36e6d6713"
    ],
    [
      "Spec.Hash.Definitions.max_input_length",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "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_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "int_typing", "lemma_Lib.IntTypes.pow2_127",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "8fb647a573198349675480c520544b92"
    ],
    [
      "Spec.Hash.Definitions.len_int_type",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "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",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "59725e4831c7f3d5d7825b20ec7340bf"
    ],
    [
      "Spec.Hash.Definitions.nat_to_len",
      1,
      2,
      1,
      [
        "@query", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned",
        "equation_Spec.Hash.Definitions.len_int_type",
        "primitive_Prims.op_Minus", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "10bd1f2751f0b768115a42a8bc38bb16"
    ],
    [
      "Spec.Hash.Definitions.len_t",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "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",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "4dd655f3b41eb3d9fb57eacb75e111b4"
    ],
    [
      "Spec.Hash.Definitions.len_v",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Spec.Hash.Definitions.Blake2B",
        "constructor_distinct_Spec.Hash.Definitions.Blake2S",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_224",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "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",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Spec.Hash.Definitions.Blake2B@tok",
        "equality_tok_Spec.Hash.Definitions.Blake2S@tok",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned",
        "equation_Spec.Hash.Definitions.len_t",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "c6e9504fe0f72a3228533c91bf0e900a"
    ],
    [
      "Spec.Hash.Definitions.len_length",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "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",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "51f331596c89dcf534098c6fa623d1d7"
    ],
    [
      "Spec.Hash.Definitions.len_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", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Spec.Hash.Definitions.Blake2B",
        "constructor_distinct_Spec.Hash.Definitions.Blake2S",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_224",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "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",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.Blake2B@tok",
        "equality_tok_Spec.Hash.Definitions.Blake2S@tok",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.len_length",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt.fits", "typing_Spec.Hash.Definitions.uu___is_MD5"
      ],
      0,
      "aa0f81d3e0fe6bf38f8ec3e713d52083"
    ],
    [
      "Spec.Hash.Definitions.len_len",
      2,
      2,
      1,
      [ "@query" ],
      0,
      "d302d6499b26a91c7b8b18afb870a774"
    ],
    [
      "Spec.Hash.Definitions.word_t",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "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",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "21fba7069922dce9e3824013afd40c76"
    ],
    [
      "Spec.Hash.Definitions.row",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.blake_alg",
        "equation_Spec.Hash.Definitions.is_blake",
        "equation_Spec.Hash.Definitions.word_t",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned",
        "typing_Spec.Hash.Definitions.is_blake",
        "typing_Spec.Hash.Definitions.word_t",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "bf61eebb1bd4f936f4cb99aefa5a910b"
    ],
    [
      "Spec.Hash.Definitions.word",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.Blake2B",
        "constructor_distinct_Spec.Hash.Definitions.Blake2S",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_224",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "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",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Spec.Hash.Definitions.Blake2S@tok",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Lib.IntTypes.unsigned",
        "equation_Spec.Hash.Definitions.is_blake",
        "equation_Spec.Hash.Definitions.word_t",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "projection_inverse_BoxBool_proj_0", "typing_Lib.IntTypes.unsigned",
        "typing_Spec.Hash.Definitions.uu___is_Blake2S",
        "typing_Spec.Hash.Definitions.uu___is_MD5",
        "typing_Spec.Hash.Definitions.uu___is_SHA2_256",
        "typing_Spec.Hash.Definitions.word_t",
        "typing_tok_Spec.Hash.Definitions.SHA2_256@tok"
      ],
      0,
      "5a70e4d7e109d8ac0db2ce724cc78715"
    ],
    [
      "Spec.Hash.Definitions.word_length",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "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",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "289a5d5293d955efeaf7f68edab6e848"
    ],
    [
      "Spec.Hash.Definitions.extra_state",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Spec.Hash.Definitions.Blake2B",
        "constructor_distinct_Spec.Hash.Definitions.Blake2S",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "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",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Spec.Hash.Definitions.Blake2S@tok",
        "equation_Lib.IntTypes.unsigned",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "projection_inverse_BoxBool_proj_0", "typing_Lib.IntTypes.unsigned",
        "typing_Spec.Hash.Definitions.uu___is_SHA2_512",
        "typing_tok_Lib.IntTypes.U128@tok"
      ],
      0,
      "6397ce7cff416b396399d4406204f799"
    ],
    [
      "Spec.Hash.Definitions.extra_state_v",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Spec.Hash.Definitions.Blake2B",
        "constructor_distinct_Spec.Hash.Definitions.Blake2S",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "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",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Spec.Hash.Definitions.Blake2B@tok",
        "equality_tok_Spec.Hash.Definitions.Blake2S@tok",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned",
        "equation_Spec.Hash.Definitions.extra_state",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "3c6db60fe3899826d0b5699e008e7f6a"
    ],
    [
      "Spec.Hash.Definitions.extra_state_int_type",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "equation_Spec.Hash.Definitions.is_blake",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe"
      ],
      0,
      "e37d3c1ff111b5f6c181e9ad1e0614b4"
    ],
    [
      "Spec.Hash.Definitions.max_extra_state",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Hash.Definitions.extra_state_int_type",
        "equation_Spec.Hash.Definitions.is_blake",
        "fuel_guarded_inversion_Lib.IntTypes.inttype",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_Spec.Hash.Definitions.extra_state_int_type",
        "typing_Spec.Hash.Definitions.is_blake"
      ],
      0,
      "b53fc3d5191f0b6c8409c475c398e30b"
    ],
    [
      "Spec.Hash.Definitions.nat_to_extra_state",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.Blake2B",
        "constructor_distinct_Spec.Hash.Definitions.Blake2S",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Spec.Hash.Definitions.Blake2B@tok",
        "equality_tok_Spec.Hash.Definitions.Blake2S@tok",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.extra_state",
        "equation_Spec.Hash.Definitions.extra_state_int_type",
        "equation_Spec.Hash.Definitions.is_blake",
        "equation_Spec.Hash.Definitions.max_extra_state", "int_inversion",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_17b5c82e827d21e595c1a46cf8137822",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe",
        "refinement_interpretation_Tm_refine_59c6c389f7d2ec9ac28044f709e4c7d6",
        "refinement_interpretation_Tm_refine_7303eab65f6a4f1e287d2ffa90e90fe1",
        "typing_Spec.Hash.Definitions.uu___is_Blake2B"
      ],
      0,
      "1c66c76c29890d02d270d90af45c5412"
    ],
    [
      "Spec.Hash.Definitions.extra_state_add_nat",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.inttype",
        "constructor_distinct_Prims.unit",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Lib.IntTypes.unsigned",
        "equation_Spec.Hash.Definitions.extra_state",
        "equation_Spec.Hash.Definitions.extra_state_int_t",
        "equation_Spec.Hash.Definitions.extra_state_int_type",
        "equation_Spec.Hash.Definitions.is_blake",
        "equation_Spec.Hash.Definitions.max_extra_state",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "refinement_interpretation_Tm_refine_028e3d676128c000131df62014b3d4df",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe",
        "typing_Lib.IntTypes.unsigned",
        "typing_Spec.Hash.Definitions.extra_state_int_type",
        "typing_Spec.Hash.Definitions.is_blake", "unit_typing"
      ],
      0,
      "ca4ddfcfdb7cc451dc77433b240aea20"
    ],
    [
      "Spec.Hash.Definitions.extra_state_add_size_t",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_pretyping_d450aafb6f125538d0e96425faddef55",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S64",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Lib.IntTypes.inttype",
        "constructor_distinct_Prims.unit", "disc_equation_Lib.IntTypes.SEC",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.op_At_Percent_Dot",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Hash.Definitions.extra_state",
        "equation_Spec.Hash.Definitions.extra_state_add_nat",
        "equation_Spec.Hash.Definitions.extra_state_int_t",
        "equation_Spec.Hash.Definitions.extra_state_int_type",
        "equation_Spec.Hash.Definitions.is_blake",
        "equation_Spec.Hash.Definitions.nat_to_extra_state",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "int_inversion", "lemma_FStar.UInt.pow2_values",
        "lemma_Lib.IntTypes.pow2_127", "lemma_Lib.IntTypes.v_injective",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe",
        "refinement_interpretation_Tm_refine_6abfdb7178db4312bbb4347133514826",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned",
        "typing_Lib.IntTypes.v", "typing_Prims.pow2",
        "typing_Spec.Hash.Definitions.extra_state_int_type",
        "typing_Spec.Hash.Definitions.is_blake",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U32@tok", "unit_typing"
      ],
      0,
      "24b3fb3281049df223df25f62d2d5898"
    ],
    [
      "Spec.Hash.Definitions.hash_word_length",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Hash.Definitions.Blake2B",
        "disc_equation_Spec.Hash.Definitions.Blake2S",
        "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",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "72fef49362c5c8da960f1ecbb7158432"
    ],
    [
      "Spec.Hash.Definitions.pad0_length",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.nonzero",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_md",
        "equation_Spec.Hash.Definitions.len_length",
        "equation_Spec.Hash.Definitions.word_length", "int_inversion",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e"
      ],
      0,
      "1ea52cac204808b9e55db4e1f819b61b"
    ],
    [
      "Spec.Hash.Definitions.pad_length",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "equation_Prims.nat", "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.is_blake",
        "equation_Spec.Hash.Definitions.is_md",
        "equation_Spec.Hash.Definitions.len_length",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "int_inversion", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2043fe1d818aaeaa104a717402baf403",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Spec.Hash.Definitions.block_length",
        "typing_Spec.Hash.Definitions.is_md",
        "typing_Spec.Hash.Definitions.len_length"
      ],
      0,
      "bc5a07358f8502cb0f0c359d10d428d4"
    ],
    [
      "Spec.Hash.Definitions.bytes_of_words",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_224",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "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",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Hash.Definitions.is_md",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_26b703b2b9201235d857bec225fb6d37",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ceeb0134124a6b2a97382acfdc508eac",
        "refinement_interpretation_Tm_refine_e78ecf464652a5ffd112c1b62bd9c25c",
        "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_Spec.Hash.Definitions.is_md",
        "typing_Spec.Hash.Definitions.uu___is_SHA2_512",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "be4bf8f118b1a31ea81caacd61c28b69"
    ],
    [
      "Spec.Hash.Definitions.bytes_of_words",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.is_md",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_e78ecf464652a5ffd112c1b62bd9c25c",
        "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "56774de7a3193efff077c8cd6874840e"
    ],
    [
      "Spec.Hash.Definitions.words_of_bytes",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_224",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "disc_equation_Lib.IntTypes.U1",
        "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",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Hash.Definitions.is_md",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_26b703b2b9201235d857bec225fb6d37",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_ceeb0134124a6b2a97382acfdc508eac",
        "refinement_interpretation_Tm_refine_e78ecf464652a5ffd112c1b62bd9c25c",
        "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_Spec.Hash.Definitions.is_md",
        "typing_Spec.Hash.Definitions.uu___is_SHA2_512",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "ba82f8c933b1c58935f3b34ff110b744"
    ],
    [
      "Spec.Hash.Definitions.words_of_bytes",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.is_md",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
        "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_e78ecf464652a5ffd112c1b62bd9c25c",
        "refinement_interpretation_Tm_refine_e7c5f4e71af26642dc90739b89f6278e",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "4e03df6d9ff05e577f1cd7634fe5cba1"
    ],
    [
      "Spec.Hash.Definitions.bytes_blocks",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_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,
      "ae7e9bbf44f4f33b9000a4c6e28f24d2"
    ],
    [
      "Spec.Hash.Definitions.pad_t",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_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,
      "bacd6fd9ac8a84b24caac8e2a753de1b"
    ]
  ]
]