[
  "û^#¶\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,
      "041f0eb81879731fa8bba9681f70ae2e"
    ],
    [
      "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,
      "ca652ca2c6708d9e84611e29526487bd"
    ],
    [
      "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,
      "78b5add557bd89f4be386c35afdee089"
    ],
    [
      "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,
      "f42a373b9179d35c25ce7003cc68c106"
    ],
    [
      "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,
      "8fb84145efe48f073b348a81aaf2f637"
    ],
    [
      "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",
        "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.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",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6",
        "typing_Spec.HMAC_DRBG.is_supported_alg"
      ],
      0,
      "80e81ddfdd97df058550f31d02595427"
    ],
    [
      "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6",
        "refinement_interpretation_Tm_refine_ca2e1245e92dc19badb6bd4080158f18",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_Spec.Hash.Definitions.word_length"
      ],
      0,
      "2faaf3c716088a6fb00d3bedc2e5cc69"
    ],
    [
      "EverCrypt.DRBG.instantiate_sha1",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equation_Spec.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "9dc080d8b3165a88bf1bfe630162c775"
    ],
    [
      "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.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "044774b81dd31f2dda96d4f6380a3fc2"
    ],
    [
      "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.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "5b14e5d0d9b7fa7378563e9174700c55"
    ],
    [
      "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.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "a9b5941eb1abe26444569916c09761cc"
    ],
    [
      "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6",
        "refinement_interpretation_Tm_refine_ca2e1245e92dc19badb6bd4080158f18",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_Spec.Hash.Definitions.word_length"
      ],
      0,
      "bb890179faa7048d7783b9f6449c5944"
    ],
    [
      "EverCrypt.DRBG.reseed_sha1",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equation_Spec.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "d5d33ad89f5407c267b31896a268afbb"
    ],
    [
      "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.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "c729ee504f2e0c0a47f2169b25b55082"
    ],
    [
      "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.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "572350697fc1bf33a4dff6c895429191"
    ],
    [
      "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.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "48541cc084649efc3f54f50a341f84cd"
    ],
    [
      "EverCrypt.DRBG.generate_st",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "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_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6",
        "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,
      "a9858781853c92aff4f8d8436ebad9b4"
    ],
    [
      "EverCrypt.DRBG.generate_sha1",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equation_Spec.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "4aeef31d423a35c5437f3228739b5679"
    ],
    [
      "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.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "fd8644e4b4b0d253a5463c8672fd0377"
    ],
    [
      "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.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "4e56b6548e726e7ca8fe72eb77444f10"
    ],
    [
      "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.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "e527badb0f99c66cbf340c990640cdd6"
    ],
    [
      "EverCrypt.DRBG.uninstantiate_sha1",
      1,
      0,
      0,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
        "equality_tok_Spec.Hash.Definitions.SHA1@tok",
        "equation_Spec.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "eb7f92f9be9593f7f548c31e0800a731"
    ],
    [
      "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.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "4ae35ccf16f86ce6cf950d97d4dd9ed9"
    ],
    [
      "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.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "a43f0a783145ee285d2bbbf7f1e79e41"
    ],
    [
      "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.HMAC_DRBG.is_supported_alg",
        "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "98c9fcb2d1435c164f89e878a99239c5"
    ]
  ]
]