[
  "گکك\"9ظ(lکج^E\b‡ٹح",
  [
    [
      "HMAC_SHA2_256.hmac_core",
      1,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqHacl.Spec.Endianness_Tm_refine_f2c63b31fd0059912139424a133143ce",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "HMAC_SHA2_256.hmac_core",
      2,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqHacl.Spec.Endianness_Tm_refine_f2c63b31fd0059912139424a133143ce",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "HMAC_SHA2_256.hmac_core",
      3,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqHacl.Spec.Endianness_Tm_refine_f2c63b31fd0059912139424a133143ce",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "HMAC_SHA2_256.hmac_core",
      4,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "HMAC_SHA2_256.hmac_core",
      5,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "data_elim_FStar.UInt32.Mk", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.mul", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.mul", "equation_FStar.UInt32.n",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
        "equation_FStar.UInt32.v", "equation_FStar.UInt8.t",
        "equation_HMAC_SHA2_256.uint8_ht", "equation_HMAC_SHA2_256.uint8_p",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_hash",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Hash.SHA2_256.size_block",
        "equation_Hacl.Hash.SHA2_256.size_block_w",
        "equation_Hacl.Hash.SHA2_256.size_hash",
        "equation_Hacl.Hash.SHA2_256.size_hash_w",
        "equation_Hacl.Hash.SHA2_256.size_word", "equation_Prims.nat",
        "equation_Spec.SHA2_256.max_input_len_8",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_len_ul_8",
        "function_token_typing_Hacl.Hash.SHA2_256.Lemmas.size_hash",
        "function_token_typing_Hacl.Hash.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "function_token_typing_Spec.SHA2_256.size_len_ul_8", "int_inversion",
        "int_typing", "kinding_FStar.UInt8.t_@tok",
        "lemma_FStar.UInt.pow2_values", "lemma_Spec.SHA2_256.pow2_values",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "proj_equation_FStar.UInt32.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.UInt32.Mk_v",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_4d0856f3239c707e1e59545e4cee6451",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_7faf017e814eb78553257c765ef9fd48",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_db529efc134cceffe51ffb5c7c317f18",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.length", "typing_FStar.UInt32.mul"
      ],
      0
    ],
    [
      "HMAC_SHA2_256.hmac_core",
      6,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt32.t",
        "equation_FStar.UInt8.t", "equation_HMAC_SHA2_256.uint32_t",
        "equation_HMAC_SHA2_256.uint8_ht", "equation_HMAC_SHA2_256.uint8_p",
        "equation_Hacl.HMAC.SHA2_256.uint8_ht",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Hash.SHA2_256.size_block",
        "equation_Hacl.Hash.SHA2_256.size_block_w",
        "equation_Hacl.Hash.SHA2_256.size_hash",
        "equation_Hacl.Hash.SHA2_256.size_hash_w",
        "equation_Hacl.Hash.SHA2_256.size_word",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_4d0856f3239c707e1e59545e4cee6451",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_7faf017e814eb78553257c765ef9fd48",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_c75b821759f73a13dc981e1f07f0650f",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_db529efc134cceffe51ffb5c7c317f18"
      ],
      0
    ],
    [
      "HMAC_SHA2_256.hmac",
      1,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqHacl.Spec.Endianness_Tm_refine_f2c63b31fd0059912139424a133143ce",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "HMAC_SHA2_256.hmac",
      2,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqHacl.Spec.Endianness_Tm_refine_f2c63b31fd0059912139424a133143ce",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "HMAC_SHA2_256.hmac",
      3,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqHMAC_SHA2_256_Tm_refine_530be526726c3b66223dd819f9d65058",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "HMAC_SHA2_256.hmac",
      4,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqHMAC_SHA2_256_Tm_refine_530be526726c3b66223dd819f9d65058",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "HMAC_SHA2_256.hmac",
      5,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "HMAC_SHA2_256.hmac",
      6,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "data_elim_FStar.UInt32.Mk", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.mul", "equation_FStar.UInt.uint_t",
        "equation_FStar.UInt32.mul", "equation_FStar.UInt32.n",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
        "equation_FStar.UInt32.v", "equation_FStar.UInt8.t",
        "equation_HMAC_SHA2_256.uint8_ht", "equation_HMAC_SHA2_256.uint8_p",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_hash",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Hash.SHA2_256.size_block",
        "equation_Hacl.Hash.SHA2_256.size_block_w",
        "equation_Hacl.Hash.SHA2_256.size_hash",
        "equation_Hacl.Hash.SHA2_256.size_hash_w",
        "equation_Hacl.Hash.SHA2_256.size_word", "equation_Prims.nat",
        "equation_Spec.SHA2_256.max_input_len_8",
        "equation_Spec.SHA2_256.size_block",
        "equation_Spec.SHA2_256.size_block_w",
        "equation_Spec.SHA2_256.size_hash",
        "equation_Spec.SHA2_256.size_hash_w",
        "equation_Spec.SHA2_256.size_len_ul_8",
        "function_token_typing_Hacl.Hash.SHA2_256.Lemmas.size_hash",
        "function_token_typing_Hacl.Hash.SHA2_256.Lemmas.size_word",
        "function_token_typing_Spec.SHA2_256.size_block",
        "function_token_typing_Spec.SHA2_256.size_hash",
        "function_token_typing_Spec.SHA2_256.size_len_ul_8", "int_inversion",
        "int_typing", "kinding_FStar.UInt8.t_@tok",
        "lemma_FStar.UInt.pow2_values", "lemma_Spec.SHA2_256.pow2_values",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "proj_equation_FStar.UInt32.Mk_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.UInt32.Mk_v",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_FStar.UInt32_Tm_refine_e27881a99184f8c07cf4428cbf7e2122",
        "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_4d0856f3239c707e1e59545e4cee6451",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_7faf017e814eb78553257c765ef9fd48",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_db529efc134cceffe51ffb5c7c317f18",
        "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_FStar.Buffer.length", "typing_FStar.UInt32.mul"
      ],
      0
    ],
    [
      "HMAC_SHA2_256.hmac",
      7,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.UInt32.t",
        "equation_FStar.UInt8.t", "equation_HMAC_SHA2_256.uint32_t",
        "equation_HMAC_SHA2_256.uint8_ht", "equation_HMAC_SHA2_256.uint8_p",
        "equation_Hacl.HMAC.SHA2_256.uint8_ht",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_block_w",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_hash_w",
        "equation_Hacl.Hash.SHA2_256.Lemmas.size_word",
        "equation_Hacl.Hash.SHA2_256.size_block",
        "equation_Hacl.Hash.SHA2_256.size_block_w",
        "equation_Hacl.Hash.SHA2_256.size_hash",
        "equation_Hacl.Hash.SHA2_256.size_hash_w",
        "equation_Hacl.Hash.SHA2_256.size_word",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_2c920a7ebd862f1908093942a4a2b626",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_4d0856f3239c707e1e59545e4cee6451",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_7faf017e814eb78553257c765ef9fd48",
        "refinement_interpretation_HMAC_SHA2_256_Tm_refine_db529efc134cceffe51ffb5c7c317f18"
      ],
      0
    ]
  ]
]