[
  "\u0011F\u000fRô;¦Ft”uøJü3N",
  [
    [
      "Hacl.Hash.Blake2.mk_update_multi",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "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",
        "equation_Hacl.Hash.Definitions.m_spec",
        "equation_Spec.Hash.Definitions.is_blake",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe"
      ],
      0,
      "7cdaaab8fd26024f906bc2b562b8c27c"
    ],
    [
      "Hacl.Hash.Blake2.mk_update_last",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "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",
        "equation_Hacl.Hash.Definitions.m_spec",
        "equation_Spec.Hash.Definitions.is_blake",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe"
      ],
      0,
      "d08c5c035849334c183093c4ace799ef"
    ],
    [
      "Hacl.Hash.Blake2.mk_hash",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@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",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Hash.Definitions.m_spec",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.Hash.Definitions.is_blake",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_550847d58e6a38975ad7c78d957daabe",
        "refinement_interpretation_Tm_refine_a0234a734e8e33a4325bad0e2485c4e2",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_Spec.Hash.Definitions.is_blake"
      ],
      0,
      "2ae7c8faca361e65985eaa133328a215"
    ]
  ]
]