[
  "�^#�\u001dȓ\u0010:\u000b\u001e��M7~",
  [
    [
      "EverCrypt.DRBG.reseed_interval",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.U32",
        "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"
      ],
      0,
      "3e9cd820f50a4fc6c09ff2a04f9f49ca"
    ],
    [
      "EverCrypt.DRBG.max_output_length",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.U32",
        "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"
      ],
      0,
      "c5b9316df8c208e89dc4c89e7c1cad42"
    ],
    [
      "EverCrypt.DRBG.max_length",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.U32",
        "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"
      ],
      0,
      "d7bbd255791a91c1f19f319f0374b7a7"
    ],
    [
      "EverCrypt.DRBG.max_personalization_string_length",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.U32",
        "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"
      ],
      0,
      "bd35fcaf7261e245a872dda454c5222e"
    ],
    [
      "EverCrypt.DRBG.max_additional_input_length",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.U32",
        "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"
      ],
      0,
      "b152c1ad3a764f723a45a6d0342b8272"
    ],
    [
      "EverCrypt.DRBG.min_length",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "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_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "equation_Spec.HMAC_DRBG.min_length",
        "equation_Spec.HMAC_DRBG.supported_alg",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
        "typing_Spec.Agile.HMAC.is_supported_alg"
      ],
      0,
      "4a4fc1af26d7e36b173a565b3dca373e"
    ],
    [
      "EverCrypt.DRBG.instantiate_st",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer",
        "equation_Prims.nat", "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_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ca2e1245e92dc19badb6bd4080158f18",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_Spec.Hash.Definitions.word_length"
      ],
      0,
      "4664cee43a3b4339fc41e8259f9a6204"
    ],
    [
      "EverCrypt.DRBG.instantiate_sha1",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "b16fe20d6afe39497e723b9a25019a96"
    ],
    [
      "EverCrypt.DRBG.instantiate_sha2_256",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "c76d17f7017460ade57836c7aef14bbf"
    ],
    [
      "EverCrypt.DRBG.instantiate_sha2_384",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "44b94ec2518f984ed5bd4f712c826359"
    ],
    [
      "EverCrypt.DRBG.instantiate_sha2_512",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "29b4f7a0309426b327997c971f997e24"
    ],
    [
      "EverCrypt.DRBG.reseed_st",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer",
        "equation_Prims.nat",
        "equation_Spec.HMAC_DRBG.max_additional_input_length",
        "equation_Spec.HMAC_DRBG.max_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_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ca2e1245e92dc19badb6bd4080158f18",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_Spec.Hash.Definitions.word_length"
      ],
      0,
      "7aa2c067096da49b27c303b39b4b3b20"
    ],
    [
      "EverCrypt.DRBG.reseed_sha1",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "2e9dc23aa1764d5b61904da32eac58e5"
    ],
    [
      "EverCrypt.DRBG.reseed_sha2_256",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "1738aef0d60ab57bec0f40876e274e81"
    ],
    [
      "EverCrypt.DRBG.reseed_sha2_384",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "930f229bab8211dff21f83e533d680ab"
    ],
    [
      "EverCrypt.DRBG.reseed_sha2_512",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "1d99b02177ec1533f79d3fbb0e25f6e3"
    ],
    [
      "EverCrypt.DRBG.generate_st",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat",
        "equation_Spec.HMAC_DRBG.max_additional_input_length",
        "equation_Spec.HMAC_DRBG.max_length",
        "equation_Spec.HMAC_DRBG.max_output_length",
        "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_Lib.IntTypes.uint8", "int_inversion",
        "int_typing", "kinding_FStar.Pervasives.Native.tuple2@tok",
        "lemma_FStar.Pervasives.invertOption",
        "lemma_FStar.UInt.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_aeb2e4ee46d14b3b648f70c9a5c878c5",
        "typing_FStar.Seq.Base.length",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.length",
        "typing_Spec.Agile.HMAC.lbytes", "typing_Spec.HMAC_DRBG.state",
        "typing_Spec.Hash.Definitions.word_length"
      ],
      0,
      "d2f7481eb94b3bdeba2c7b51fa0d64f4"
    ],
    [
      "EverCrypt.DRBG.generate_sha1",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "1f3778cb7b3f790d3100faa2483b1c3f"
    ],
    [
      "EverCrypt.DRBG.generate_sha2_256",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "25c4472221cb53bf3b5593a1a7ddb57f"
    ],
    [
      "EverCrypt.DRBG.generate_sha2_384",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "ce23680fdfe20e6dd460adfbbaf78a3c"
    ],
    [
      "EverCrypt.DRBG.generate_sha2_512",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "9ac74fbecae009e2ce07ddce8b453990"
    ],
    [
      "EverCrypt.DRBG.uninstantiate_sha1",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "42c0ac98001a4598b39de209e77e780a"
    ],
    [
      "EverCrypt.DRBG.uninstantiate_sha2_256",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
        "equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "c7413b9e5b3d310022512152d646443a"
    ],
    [
      "EverCrypt.DRBG.uninstantiate_sha2_384",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_384",
        "equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "058a7ce6c1344a83564bac2e85eca2c0"
    ],
    [
      "EverCrypt.DRBG.uninstantiate_sha2_512",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Spec.Agile.HMAC.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "06c0a0d31aece0b34f5fa203ff1dc7ad"
    ]
  ]
]