[
  "³UÁ\u0001Þ‚L´¿‡v7µ¤of",
  [
    [
      "Hacl.Hash.SHA2.hash_512_lib",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.uint8", "equation_Prims.nat",
        "function_token_typing_Lib.IntTypes.uint8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_ba6535c81ac79c73069a58071022c688",
        "typing_Lib.Buffer.length", "typing_tok_Lib.Buffer.MUT@tok"
      ],
      0,
      "5857480679b87f7e551958e688e17d54"
    ]
  ]
]