[
  "ŻĄˇlKAybꤍ˛œôE€",
  [
    [
      "Hacl.HMAC_DRBG.reseed_interval",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W31",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W31@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0"
      ],
      0,
      "b260081ec4c6a2aaf40178001b823eb7"
    ],
    [
      "Hacl.HMAC_DRBG.max_output_length",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W31",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W31@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0"
      ],
      0,
      "8132660df0d242ba584b969d82728676"
    ],
    [
      "Hacl.HMAC_DRBG.max_length",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W31",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W31@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0"
      ],
      0,
      "90dcfe61b618f588dbbffd4b253d8d7c"
    ],
    [
      "Hacl.HMAC_DRBG.max_personalization_string_length",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W31",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W31@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0"
      ],
      0,
      "abdd9fd59ed7d10b818ccfff08c5c90f"
    ],
    [
      "Hacl.HMAC_DRBG.max_additional_input_length",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W31",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W31@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0"
      ],
      0,
      "217b6d5e30424c3bb2b3436f0a87ad46"
    ],
    [
      "Hacl.HMAC_DRBG.min_length",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W32",
        "constructor_distinct_FStar.Integers.W64",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_FStar.Integers.Winfinite",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "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",
        "disc_equation_Spec.Hash.Definitions.SHA1",
        "disc_equation_Spec.Hash.Definitions.SHA2_256",
        "disc_equation_Spec.Hash.Definitions.SHA2_384",
        "disc_equation_Spec.Hash.Definitions.SHA2_512",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W64@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_FStar.Integers.Winfinite@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
        "equation_Spec.HMAC_DRBG.is_supported_alg",
        "equation_Spec.HMAC_DRBG.min_length",
        "equation_Spec.HMAC_DRBG.supported_alg",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_Spec.HMAC_DRBG.is_supported_alg"
      ],
      0,
      "4295b8d7e8b10e010223a0322cc54bce"
    ],
    [
      "Hacl.HMAC_DRBG.instantiate_st",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W32",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_FStar.Integers.Winfinite",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_FStar.Integers.Winfinite@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U1@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.HMAC_DRBG.max_length", "equation_Lib.Buffer.as_seq",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
        "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.max_length",
        "equation_Spec.HMAC_DRBG.max_personalization_string_length",
        "equation_Spec.HMAC_DRBG.supported_alg",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_Lib.IntTypes.uint8", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_4de060dc512b2b2bb293cc7109bdc63f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_b208150486e442bda22e11bfc7be5426",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
        "typing_Hacl.HMAC_DRBG.max_length", "typing_Lib.Buffer.as_seq",
        "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
        "typing_Spec.Hash.Definitions.word_length",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "c539cad6e7994e0a81302f206aa86521"
    ],
    [
      "Hacl.HMAC_DRBG.reseed_st",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W32",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_FStar.Integers.Winfinite",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_FStar.Integers.Winfinite@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "equation_Spec.HMAC_DRBG.supported_alg",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_Spec.AES.elem", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.Buffer.as_seq", "typing_Lib.IntTypes.v",
        "typing_Spec.Hash.Definitions.word_length",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "a103373d31140e39ca2a0a271125ffa4"
    ],
    [
      "Hacl.HMAC_DRBG.generate_st",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_FStar.Integers.W16",
        "constructor_distinct_FStar.Integers.W32",
        "constructor_distinct_FStar.Integers.W8",
        "constructor_distinct_FStar.Integers.Winfinite",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_FStar.Integers.W16@tok",
        "equality_tok_FStar.Integers.W32@tok",
        "equality_tok_FStar.Integers.W8@tok",
        "equality_tok_FStar.Integers.Winfinite@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
        "equation_Lib.Sequence.lseq", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "equation_Spec.HMAC_DRBG.supported_alg",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_Prims.int",
        "function_token_typing_Spec.AES.elem",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "kinding_FStar.Pervasives.Native.tuple2@tok",
        "lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Addition",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Integers.Signed__0",
        "projection_inverse_FStar.Integers.Unsigned__0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0b526a150094479a2e4a673f2662a197",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6",
        "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length",
        "typing_Lib.IntTypes.v", "typing_Spec.Agile.HMAC.lbytes",
        "typing_Spec.HMAC_DRBG.state",
        "typing_Spec.Hash.Definitions.word_length",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5a662528c68d83e56d681b7e400b812c"
    ]
  ]
]