[
  "®Ýþ\u0012zÙ0†–apj— Dó",
  [
    [
      "Hacl.Hash.Blake2.Lemmas.blake2_init_no_key_is_agile",
      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.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Blake2.Blake2B",
        "constructor_distinct_Spec.Blake2.Blake2S",
        "constructor_distinct_Spec.Hash.Definitions.Blake2B",
        "constructor_distinct_Spec.Hash.Definitions.Blake2S",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Blake2.Blake2B@tok",
        "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Blake2.max_key", "equation_Spec.Blake2.max_output",
        "equation_Spec.Blake2.wt",
        "equation_Spec.Hash.Definitions.blake_alg",
        "equation_Spec.Hash.Definitions.is_blake",
        "equation_Spec.Hash.Definitions.max_extra_state",
        "equation_Spec.Hash.Definitions.row",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.to_blake_alg",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_Spec.Hash.Definitions.is_blake",
        "typing_Spec.Hash.Definitions.max_extra_state",
        "typing_Spec.Hash.Definitions.to_blake_alg",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "4025653d34871d654bdfcfe3c7c9319c"
    ],
    [
      "Hacl.Hash.Blake2.Lemmas.lemma_blake2_hash_equivalence",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "Spec.Blake2_pretyping_db784d5da91640e63403e359daacba94",
        "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.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_Prims.unit",
        "constructor_distinct_Spec.Blake2.Blake2B",
        "constructor_distinct_Spec.Blake2.Blake2S",
        "constructor_distinct_Spec.Blake2.alg",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Blake2.Blake2B@tok",
        "equality_tok_Spec.Blake2.Blake2S@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Blake2.max_key",
        "equation_Spec.Blake2.max_limb", "equation_Spec.Blake2.max_output",
        "equation_Spec.Blake2.wt",
        "equation_Spec.Hash.Definitions.blake_alg",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.is_blake",
        "equation_Spec.Hash.Definitions.max_input_length",
        "equation_Spec.Hash.Definitions.to_blake_alg",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.Blake2.alg",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_8f4f0e1bdbf271008dd9328cde2d4929",
        "typing_Lib.IntTypes.bits", "typing_Prims.pow2",
        "typing_Spec.Hash.Definitions.is_blake",
        "typing_Spec.Hash.Definitions.to_blake_alg",
        "typing_tok_Lib.IntTypes.U32@tok", "unit_typing"
      ],
      0,
      "a6ea6912b5f1a84acd9dab5371a82bca"
    ],
    [
      "Hacl.Hash.Blake2.Lemmas.update_multi_add_extra",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.l_and", "equation_Prims.squash", "l_and-interp",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "28e4cb3e06fc296847bd3270a2bb9d2f"
    ]
  ]
]