[
  "�r\n�D��6]\t/y)I4�",
  [
    [
      "EverCrypt.HMAC.compute_st",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_EverCrypt.Helpers.uint8_p",
        "equation_EverCrypt.Helpers.uint8_t",
        "equation_LowStar.Buffer.buffer",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.max_input_length",
        "equation_Spec.Hash.Definitions.word_length",
        "fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
        "function_token_typing_FStar.UInt8.t",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0879c107c66fba8772fecae610c19578",
        "refinement_interpretation_Tm_refine_d31cd115930e46a8b73a31bb5e929899",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "5cad2935654f325bab5679ccd593fecf"
    ]
  ]
]