[
  "As]�H\u001c\u0007Y�8C�p|�P",
  [
    [
      "EverCrypt.HMAC.ha",
      1,
      2,
      1,
      [ "@query", "assumption_Spec.Hash.Definitions.hash_alg__uu___haseq" ],
      0,
      "ca1df55032a1ccec7136ccc23b18c205"
    ],
    [
      "EverCrypt.HMAC.lbytes",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "function_token_typing_Prims.int",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "d1cf09af54c6145e0cb95fef6e6ffff3"
    ],
    [
      "EverCrypt.HMAC.hmac",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.state_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,
      "91a20e4d221da044cdcbad10c55284f5"
    ],
    [
      "EverCrypt.HMAC.compute_st",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_FStar.Integers.Signed",
        "constructor_distinct_FStar.Integers.Winfinite",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "equality_tok_FStar.Integers.Winfinite@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@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_EverCrypt.HMAC.ha", "equation_EverCrypt.Helpers.uint8_p",
        "equation_EverCrypt.Helpers.uint8_t",
        "equation_FStar.Integers.int_t", "equation_LowStar.Buffer.buffer",
        "equation_Prims.nat", "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_FStar.UInt8.t",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "refinement_interpretation_Tm_refine_0879c107c66fba8772fecae610c19578",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_bd8e34d3b91921b2fb6a6503e772851a",
        "refinement_interpretation_Tm_refine_ebffc3f6e29e8ccae641682a151feefa",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_Spec.Hash.Definitions.word_length"
      ],
      0,
      "586a475d5c2d0da2819d8d12f0ab59fd"
    ]
  ]
]