[ "RyB^K\u0002$'", [ [ "EverCrypt.DRBG.reseed_interval", 1, 2, 1, [ "@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, "14d43b9a1fd8563a83be37f512de82aa" ], [ "EverCrypt.DRBG.max_output_length", 1, 2, 1, [ "@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, "23118a875c77b859dec227b71dc5e872" ], [ "EverCrypt.DRBG.max_length", 1, 2, 1, [ "@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, "d9da6a91d2c7d35e9ef9803ea47e234a" ], [ "EverCrypt.DRBG.max_personalization_string_length", 1, 2, 1, [ "@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, "d72ad2b3653256581d6e5ebcff261d8b" ], [ "EverCrypt.DRBG.max_additional_input_length", 1, 2, 1, [ "@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, "421aad0a22944944d19610567edd712f" ], [ "EverCrypt.DRBG.min_length", 1, 2, 1, [ "@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, "417750591ae0377acfee1a3d91261ac3" ], [ "EverCrypt.DRBG.state_s", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_FStar.Integers.W32@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "1d1e16c2184fca5ab4a8d4469ec44da9" ], [ "EverCrypt.DRBG.state_s", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_FStar.Integers.W32@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "139ac8c50824b50798514b2f23cdd2a8" ], [ "EverCrypt.DRBG.state_s", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "962c4f150813e5ee8842407ef50d59b6" ], [ "EverCrypt.DRBG.state_s", 4, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "2459b72ebc62f1b1f1c33dc1fe2d1a4b" ], [ "EverCrypt.DRBG.state_s", 5, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "ca8afe4fff01c3f92422726dc1a40a0f" ], [ "EverCrypt.DRBG.state_s", 6, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "f9b29dff85c0c82935fbc4821fbba876" ], [ "EverCrypt.DRBG.state_s", 7, 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, "68084263ad1120c4632c5bc32f2e27a4" ], [ "EverCrypt.DRBG.state_s", 8, 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, "3c1bb821c4f7462c7a1063d8ff7cb50c" ], [ "EverCrypt.DRBG.__proj__SHA1_s__item___0", 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, "f1769a72dbdb20f8ef6a0dbd623ee37e" ], [ "EverCrypt.DRBG.__proj__SHA1_s__item___0", 2, 0, 0, [ "@MaxIFuel_assumption", "@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", "refinement_interpretation_Tm_refine_0e97eceb5a4fa3473c9281e4e259d6ff" ], 0, "6a95e00bfe85ef2ce53be058f3713ab9" ], [ "EverCrypt.DRBG.__proj__SHA2_256_s__item___0", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "disc_equation_EverCrypt.DRBG.SHA2_256_s", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Spec.HMAC_DRBG.is_supported_alg", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_31cbfb78bf9a2736dec227846252ef73" ], 0, "0467a83439dea4bce5f3ce8a60dc76ea" ], [ "EverCrypt.DRBG.__proj__SHA2_256_s__item___0", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "disc_equation_EverCrypt.DRBG.SHA2_256_s", "equality_tok_FStar.Integers.W64@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Spec.HMAC_DRBG.is_supported_alg", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_31cbfb78bf9a2736dec227846252ef73" ], 0, "b6d6db74ed30de680d3392144292737a" ], [ "EverCrypt.DRBG.__proj__SHA2_384_s__item___0", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "disc_equation_EverCrypt.DRBG.SHA2_384_s", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Spec.HMAC_DRBG.is_supported_alg", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_48725dc4965c47559da6abe7dbe84cfb" ], 0, "82809081bb4b51f94e4fcccc3a888b02" ], [ "EverCrypt.DRBG.__proj__SHA2_384_s__item___0", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "disc_equation_EverCrypt.DRBG.SHA2_384_s", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Spec.HMAC_DRBG.is_supported_alg", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_48725dc4965c47559da6abe7dbe84cfb" ], 0, "c15f427599f66d34108143cb385b0de7" ], [ "EverCrypt.DRBG.__proj__SHA2_512_s__item___0", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "disc_equation_EverCrypt.DRBG.SHA2_512_s", "equality_tok_FStar.Integers.W32@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Spec.HMAC_DRBG.is_supported_alg", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_c51a2c9d00ea095bc4546df321dd3dae" ], 0, "b74164777ef91779dc0633cfb5e8bf35" ], [ "EverCrypt.DRBG.__proj__SHA2_512_s__item___0", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "disc_equation_EverCrypt.DRBG.SHA2_512_s", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W32@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Spec.HMAC_DRBG.is_supported_alg", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_c51a2c9d00ea095bc4546df321dd3dae" ], 0, "bb611483e4bf5dde5270a192c3cb13a6" ], [ "EverCrypt.DRBG.p", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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_EverCrypt.DRBG.SHA1_s", "disc_equation_EverCrypt.DRBG.SHA2_256_s", "disc_equation_EverCrypt.DRBG.SHA2_384_s", "disc_equation_EverCrypt.DRBG.SHA2_512_s", "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_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_Spec.Agile.HMAC.is_supported_alg", "equation_Spec.HMAC_DRBG.supported_alg", "fuel_guarded_inversion_EverCrypt.DRBG.state_s", "inversion-interp", "lemma_EverCrypt.DRBG.invert_state_s", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574", "typing_Spec.Agile.HMAC.is_supported_alg" ], 0, "5b50fdbde4bbe51205792741fef149a6" ], [ "EverCrypt.DRBG.repr", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_EverCrypt.DRBG.state", "equation_LowStar.Buffer.pointer", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e" ], 0, "4aa8a1e97568878e2fd1a7c49dcf2f1d" ], [ "EverCrypt.DRBG.loc_includes_union_l_footprint_s", 1, 0, 0, [ "@query" ], 0, "63fbff23a666adad9f2a008c0581d9fb" ], [ "EverCrypt.DRBG.invariant_loc_in_footprint", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_typing", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equation_EverCrypt.DRBG.footprint", "equation_EverCrypt.DRBG.footprint_s", "equation_EverCrypt.DRBG.invariant", "equation_EverCrypt.DRBG.invariant_s", "equation_EverCrypt.DRBG.p", "equation_EverCrypt.DRBG.state", "equation_Hacl.HMAC_DRBG.footprint", "equation_Hacl.HMAC_DRBG.invariant", "equation_Hacl.Hash.Definitions.hash_len", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.live", "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.Monotonic.Buffer.loc_in", "equation_Prims.eqtype", "equation_Prims.nat", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing", "kinding_EverCrypt.DRBG.state_s@tok", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "proj_equation_Hacl.HMAC_DRBG.State_k", "proj_equation_Hacl.HMAC_DRBG.State_reseed_counter", "proj_equation_Hacl.HMAC_DRBG.State_v", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4b484af68eae8d74dfeb59bfc788394f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.DRBG.footprint_s", "typing_EverCrypt.DRBG.p", "typing_FStar.Set.singleton", "typing_Hacl.HMAC_DRBG.__proj__State__item__k", "typing_Hacl.HMAC_DRBG.__proj__State__item__reseed_counter", "typing_Hacl.HMAC_DRBG.__proj__State__item__v", "typing_Lib.Buffer.union", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.get", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in" ], 0, "7186a0229f2eb1d1eb1f1800bbacced4" ], [ "EverCrypt.DRBG.frame_invariant", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W31", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W31@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_EverCrypt.DRBG.footprint", "equation_EverCrypt.DRBG.footprint_s", "equation_EverCrypt.DRBG.invariant", "equation_EverCrypt.DRBG.invariant_s", "equation_EverCrypt.DRBG.p", "equation_EverCrypt.DRBG.repr", "equation_EverCrypt.DRBG.state", "equation_Hacl.HMAC_DRBG.footprint", "equation_Hacl.HMAC_DRBG.invariant", "equation_Hacl.HMAC_DRBG.repr", "equation_Hacl.Hash.Definitions.hash_len", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.bget", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.Agile.HMAC.is_supported_alg", "equation_Spec.HMAC_DRBG.supported_alg", "fuel_guarded_inversion_Hacl.HMAC_DRBG.state", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing", "kinding_EverCrypt.DRBG.state_s@tok", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "proj_equation_Hacl.HMAC_DRBG.State_k", "proj_equation_Hacl.HMAC_DRBG.State_reseed_counter", "proj_equation_Hacl.HMAC_DRBG.State_v", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4b484af68eae8d74dfeb59bfc788394f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.DRBG.footprint_s", "typing_EverCrypt.DRBG.p", "typing_FStar.Set.singleton", "typing_Hacl.HMAC_DRBG.__proj__State__item__k", "typing_Hacl.HMAC_DRBG.__proj__State__item__reseed_counter", "typing_Hacl.HMAC_DRBG.__proj__State__item__v", "typing_Hacl.Hash.Definitions.hash_len", "typing_Lib.Buffer.loc", "typing_Lib.Buffer.union", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.get", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.Agile.HMAC.is_supported_alg", "typing_tok_Lib.Buffer.MUT@tok" ], 0, "315c21b21401a464c883a25811fe7435" ], [ "EverCrypt.DRBG.alloca", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_EverCrypt.DRBG.SHA1_s", "constructor_distinct_EverCrypt.DRBG.SHA2_256_s", "constructor_distinct_EverCrypt.DRBG.SHA2_384_s", "constructor_distinct_EverCrypt.DRBG.SHA2_512_s", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "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_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", "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.DRBG.footprint", "equation_EverCrypt.DRBG.footprint_s", "equation_EverCrypt.DRBG.invariant", "equation_EverCrypt.DRBG.invariant_s", "equation_EverCrypt.DRBG.p", "equation_EverCrypt.DRBG.state", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_stack_region", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Hacl.HMAC_DRBG.footprint", "equation_Hacl.HMAC_DRBG.invariant", "equation_Hacl.Hash.Definitions.hash_len", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.live", "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "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.is_supported_alg", "equation_Spec.HMAC_DRBG.supported_alg", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Prims.int", "function_token_typing_Spec.AES.elem", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "kinding_EverCrypt.DRBG.state_s@tok", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_addresses_", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_GreaterThan", "proj_equation_Hacl.HMAC_DRBG.State_k", "proj_equation_Hacl.HMAC_DRBG.State_reseed_counter", "proj_equation_Hacl.HMAC_DRBG.State_v", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_EverCrypt.DRBG.SHA1_s__0", "projection_inverse_EverCrypt.DRBG.SHA2_256_s__0", "projection_inverse_EverCrypt.DRBG.SHA2_384_s__0", "projection_inverse_EverCrypt.DRBG.SHA2_512_s__0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4b484af68eae8d74dfeb59bfc788394f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_f578aa678648488fdd6f0421fc6e423d", "refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.DRBG.footprint_s", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Set.singleton", "typing_FStar.UInt32.t", "typing_Hacl.HMAC_DRBG.__proj__State__item__k", "typing_Hacl.HMAC_DRBG.__proj__State__item__reseed_counter", "typing_Hacl.HMAC_DRBG.__proj__State__item__v", "typing_Hacl.HMAC_DRBG.footprint", "typing_Lib.Buffer.length", "typing_Lib.Buffer.union", "typing_Lib.IntTypes.minint", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.get", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_unused_in", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.HMAC_DRBG.is_supported_alg", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "be0744c5e4c3aff98bc732f97f5dc4a7" ], [ "EverCrypt.DRBG.create_in", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_EverCrypt.DRBG.SHA1_s", "constructor_distinct_EverCrypt.DRBG.SHA2_256_s", "constructor_distinct_EverCrypt.DRBG.SHA2_384_s", "constructor_distinct_EverCrypt.DRBG.SHA2_512_s", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "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_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", "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.DRBG.footprint", "equation_EverCrypt.DRBG.footprint_s", "equation_EverCrypt.DRBG.freeable", "equation_EverCrypt.DRBG.freeable_s", "equation_EverCrypt.DRBG.invariant", "equation_EverCrypt.DRBG.invariant_s", "equation_EverCrypt.DRBG.p", "equation_EverCrypt.DRBG.state", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_heap_color", "equation_FStar.Monotonic.HyperStack.mem", "equation_Hacl.HMAC_DRBG.footprint", "equation_Hacl.HMAC_DRBG.freeable", "equation_Hacl.HMAC_DRBG.invariant", "equation_Hacl.Hash.Definitions.hash_len", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.fresh_loc", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "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.is_supported_alg", "equation_Spec.HMAC_DRBG.supported_alg", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Prims.int", "function_token_typing_Spec.AES.elem", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "kinding_EverCrypt.DRBG.state_s@tok", "l_and-interp", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Seq.Base.lemma_index_create", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.freeable_length", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_addresses_", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_Negation", "proj_equation_Hacl.HMAC_DRBG.State_k", "proj_equation_Hacl.HMAC_DRBG.State_reseed_counter", "proj_equation_Hacl.HMAC_DRBG.State_v", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_EverCrypt.DRBG.SHA1_s__0", "projection_inverse_EverCrypt.DRBG.SHA2_256_s__0", "projection_inverse_EverCrypt.DRBG.SHA2_384_s__0", "projection_inverse_EverCrypt.DRBG.SHA2_512_s__0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_161e04719814801d293219f408210f95", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4294b22173f6792d1a33bbae93cc5288", "refinement_interpretation_Tm_refine_4b484af68eae8d74dfeb59bfc788394f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.DRBG.footprint_s", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.color", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.is_heap_color", "typing_FStar.Set.singleton", "typing_FStar.UInt32.t", "typing_Hacl.HMAC_DRBG.__proj__State__item__k", "typing_Hacl.HMAC_DRBG.__proj__State__item__reseed_counter", "typing_Hacl.HMAC_DRBG.__proj__State__item__v", "typing_Hacl.HMAC_DRBG.footprint", "typing_Lib.Buffer.length", "typing_Lib.Buffer.union", "typing_Lib.IntTypes.minint", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.get", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_unused_in", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.HMAC_DRBG.is_supported_alg", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "b3819eb73123d22d1db4caa8f409951b" ], [ "EverCrypt.DRBG.create", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Monotonic.HyperStack.is_heap_color", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Spec.Agile.HMAC.is_supported_alg", "equation_Spec.HMAC_DRBG.supported_alg", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_f759b00d0ea3017d744ed132c2ce48f4", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_Spec.Agile.HMAC.is_supported_alg" ], 0, "304e65b5d0878009a412627f18893232" ], [ "EverCrypt.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.PUB", "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.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.DRBG.state", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "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", "kinding_EverCrypt.DRBG.state_s@tok", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "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_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6", "refinement_interpretation_Tm_refine_ca2e1245e92dc19badb6bd4080158f18", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.word_length" ], 0, "28390a18068343e6e774bf95fad27aaa" ], [ "EverCrypt.DRBG.mk_instantiate", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Tm_unit", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "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", "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.DRBG.disjoint_st", "equation_EverCrypt.DRBG.footprint", "equation_EverCrypt.DRBG.footprint_s", "equation_EverCrypt.DRBG.freeable", "equation_EverCrypt.DRBG.invariant", "equation_EverCrypt.DRBG.invariant_s", "equation_EverCrypt.DRBG.p", "equation_EverCrypt.DRBG.preserves_freeable", "equation_EverCrypt.DRBG.repr", "equation_EverCrypt.DRBG.state", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Int.op_Slash", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.HMAC_DRBG.footprint", "equation_Hacl.HMAC_DRBG.invariant", "equation_Hacl.HMAC_DRBG.max_length", "equation_Hacl.HMAC_DRBG.max_personalization_string_length", "equation_Hacl.HMAC_DRBG.min_length", "equation_Hacl.HMAC_DRBG.repr", "equation_Hacl.Hash.Definitions.hash_len", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.bget", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1", "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.abs", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Agile.HMAC.is_supported_alg", "equation_Spec.HMAC_DRBG.instantiate", "equation_Spec.HMAC_DRBG.max_personalization_string_length", "equation_Spec.HMAC_DRBG.min_length", "equation_Spec.HMAC_DRBG.supported_alg", "fuel_guarded_inversion_Hacl.HMAC_DRBG.state", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "kinding_EverCrypt.DRBG.state_s@tok", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.lemma_equal_refl", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.div_lemma", "lemma_Lib.IntTypes.gt_lemma", "lemma_Lib.IntTypes.pow2_4", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.len_gsub", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_gsub", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_Hacl.HMAC_DRBG.State_k", "proj_equation_Hacl.HMAC_DRBG.State_reseed_counter", "proj_equation_Hacl.HMAC_DRBG.State_v", "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.HMAC_DRBG.State_k", "projection_inverse_Spec.HMAC_DRBG.State_reseed_counter", "projection_inverse_Spec.HMAC_DRBG.State_v", "refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_14aab2321e74365959b67105c3406f1a", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4b484af68eae8d74dfeb59bfc788394f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56f50ac9b2c01fabfe5c20434e382627", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_60e818fdc2ee6352881389f80885c1a1", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7e86f8eacba37cea734281899965ca92", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_89a8faea474f01a49f61f4487fc1d44c", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_b208150486e442bda22e11bfc7be5426", "refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_interpretation_Tm_refine_c41a25eac56456a928dba09456893697", "refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde", "refinement_interpretation_Tm_refine_ca2e1245e92dc19badb6bd4080158f18", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_d98668fdeb0d6f2966f644695bb84d19", "refinement_interpretation_Tm_refine_e450d0eda8ec6ce5c9eff42d01f0e81a", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Prims.pow2.fuel_instrumented", "true_interp", "typing_EverCrypt.DRBG.footprint", "typing_EverCrypt.DRBG.footprint_s", "typing_EverCrypt.DRBG.p", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Map.upd", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.mk_mem", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.HMAC_DRBG.__proj__State__item__k", "typing_Hacl.HMAC_DRBG.__proj__State__item__reseed_counter", "typing_Hacl.HMAC_DRBG.__proj__State__item__v", "typing_Hacl.HMAC_DRBG.max_length", "typing_Hacl.HMAC_DRBG.max_personalization_string_length", "typing_Hacl.HMAC_DRBG.min_length", "typing_Hacl.Hash.Definitions.hash_len", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.loc", "typing_Lib.Buffer.union", "typing_Lib.IntTypes.add", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.maxint", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.pub_int_v", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.get", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Prims.pow2", "typing_Spec.Agile.HMAC.is_supported_alg", "typing_Spec.HMAC_DRBG.min_length", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "1bb63a882d7c46fb354a0a7d249bd5c9" ], [ "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, "f7e95a8576fd604000bdf8dc1e12f1b9" ], [ "EverCrypt.DRBG.instantiate_sha1", 2, 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, "bbce5e79fbe5ea98031009587a24f045" ], [ "EverCrypt.DRBG.instantiate_sha2_256", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "d3ae199621f8a819ac4f2dfe98ac389b" ], [ "EverCrypt.DRBG.instantiate_sha2_256", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "7c1bab6ea5b445329699b729a9c3880c" ], [ "EverCrypt.DRBG.instantiate_sha2_384", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "c704a67e4d6b5b57fa1858913292d922" ], [ "EverCrypt.DRBG.instantiate_sha2_384", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "810dbf4cc224016ffd69bcdd4016d9c1" ], [ "EverCrypt.DRBG.instantiate_sha2_512", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_FStar.Integers.W32@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "0327870a739afd5baeb3e39530e5c7bb" ], [ "EverCrypt.DRBG.instantiate_sha2_512", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_FStar.Integers.W32@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "a317daca13450789600063b3d9d03fb2" ], [ "EverCrypt.DRBG.reseed_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.PUB", "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.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.DRBG.state", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "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", "kinding_EverCrypt.DRBG.state_s@tok", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "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_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_ca2e1245e92dc19badb6bd4080158f18", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.word_length", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "f993d9317d422f1162193bd143cea874" ], [ "EverCrypt.DRBG.mk_reseed", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W31", "constructor_distinct_FStar.Integers.W63", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "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", "constructor_distinct_Tm_unit", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W31@tok", "equality_tok_FStar.Integers.W63@tok", "equality_tok_FStar.Integers.W8@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", "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.DRBG.disjoint_st", "equation_EverCrypt.DRBG.footprint", "equation_EverCrypt.DRBG.footprint_s", "equation_EverCrypt.DRBG.freeable", "equation_EverCrypt.DRBG.invariant", "equation_EverCrypt.DRBG.invariant_s", "equation_EverCrypt.DRBG.p", "equation_EverCrypt.DRBG.preserves_freeable", "equation_EverCrypt.DRBG.repr", "equation_EverCrypt.DRBG.state", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_FStar.Seq.Base.op_At_Bar", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.HMAC_DRBG.disjoint_st", "equation_Hacl.HMAC_DRBG.footprint", "equation_Hacl.HMAC_DRBG.invariant", "equation_Hacl.HMAC_DRBG.max_additional_input_length", "equation_Hacl.HMAC_DRBG.max_length", "equation_Hacl.HMAC_DRBG.min_length", "equation_Hacl.HMAC_DRBG.repr", "equation_Hacl.Hash.Definitions.hash_len", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.bget", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1", "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_LowStar.Monotonic.Buffer.loc_in", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Agile.HMAC.is_supported_alg", "equation_Spec.HMAC_DRBG.max_additional_input_length", "equation_Spec.HMAC_DRBG.min_length", "equation_Spec.HMAC_DRBG.reseed", "equation_Spec.HMAC_DRBG.supported_alg", "equation_Spec.Hash.Definitions.bytes", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_EverCrypt.DRBG.state_s", "fuel_guarded_inversion_Hacl.HMAC_DRBG.state", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "inversion-interp", "kinding_EverCrypt.DRBG.state_s@tok", "lemma_EverCrypt.DRBG.invariant_loc_in_footprint", "lemma_EverCrypt.DRBG.invert_state_s", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.lemma_equal_refl", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_Lib.Buffer.modifies_preserves_live", "lemma_Lib.IntTypes.gt_lemma", "lemma_Lib.IntTypes.v_mk_int", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "proj_equation_Hacl.HMAC_DRBG.State_k", "proj_equation_Hacl.HMAC_DRBG.State_reseed_counter", "proj_equation_Hacl.HMAC_DRBG.State_v", "proj_equation_Spec.HMAC_DRBG.State_k", "proj_equation_Spec.HMAC_DRBG.State_v", "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.HMAC_DRBG.State_k", "projection_inverse_Spec.HMAC_DRBG.State_reseed_counter", "projection_inverse_Spec.HMAC_DRBG.State_v", "refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_061f9c7bfe87cc1c05d810348a7856e8", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_3ec181c4950a228cbbd4613a357d831e", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4b484af68eae8d74dfeb59bfc788394f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_60e818fdc2ee6352881389f80885c1a1", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7e86f8eacba37cea734281899965ca92", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_b208150486e442bda22e11bfc7be5426", "refinement_interpretation_Tm_refine_bd307bf4af18b48116192667829bd5c7", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde", "refinement_interpretation_Tm_refine_ca2e1245e92dc19badb6bd4080158f18", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fa09e05a8794568dd6601ad6c5428df1", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.DRBG.footprint", "typing_EverCrypt.DRBG.footprint_s", "typing_EverCrypt.DRBG.p", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Map.upd", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.mk_mem", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt32.v", "typing_Hacl.HMAC_DRBG.__proj__State__item__k", "typing_Hacl.HMAC_DRBG.__proj__State__item__reseed_counter", "typing_Hacl.HMAC_DRBG.__proj__State__item__v", "typing_Hacl.HMAC_DRBG.max_additional_input_length", "typing_Hacl.HMAC_DRBG.max_length", "typing_Hacl.HMAC_DRBG.min_length", "typing_Hacl.Hash.Definitions.hash_len", "typing_Lib.Buffer.loc", "typing_Lib.Buffer.union", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.get", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Prims.pow2", "typing_Spec.Agile.HMAC.is_supported_alg", "typing_Spec.HMAC_DRBG.min_length", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "817d9fe112adf5fc15b8ad4d904c9a1b" ], [ "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, "c0c05e310d4c86104475fe91325d4134" ], [ "EverCrypt.DRBG.reseed_sha1", 2, 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, "14a4b8c1fbec896c84da31c1d17fc6c0" ], [ "EverCrypt.DRBG.reseed_sha2_256", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "ba0c95aa321e6365f20403b44f286ddd" ], [ "EverCrypt.DRBG.reseed_sha2_256", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "da9be11b77c84ee0de9b91dceb0336c3" ], [ "EverCrypt.DRBG.reseed_sha2_384", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "6541387bd4b8040c46d25e381c120108" ], [ "EverCrypt.DRBG.reseed_sha2_384", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "daf87902c8c39a30163e5d8956298e86" ], [ "EverCrypt.DRBG.reseed_sha2_512", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_FStar.Integers.W32@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "e4d757709be5c4b962cc76ccb45228b5" ], [ "EverCrypt.DRBG.reseed_sha2_512", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_FStar.Integers.W32@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "00f03d5650ba910de47239ee35ec8f16" ], [ "EverCrypt.DRBG.generate_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.PUB", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_FStar.Pervasives.Native.None", "disc_equation_FStar.Pervasives.Native.Some", "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.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equation_EverCrypt.DRBG.state", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "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.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", "function_token_typing_Spec.AES.elem", "int_inversion", "int_typing", "kinding_EverCrypt.DRBG.state_s@tok", "kinding_FStar.Pervasives.Native.tuple2@tok", "kinding_Spec.HMAC_DRBG.state@tok", "lemma_FStar.Pervasives.invertOption", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "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_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6", "refinement_interpretation_Tm_refine_aeb2e4ee46d14b3b648f70c9a5c878c5", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.length", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.length", "typing_Spec.AES.gf8", "typing_Spec.Agile.HMAC.lbytes", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.word_length" ], 0, "fa0f1b86eccceac4f6d100565e8efdd0" ], [ "EverCrypt.DRBG.mk_generate", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Pervasives.Native.Some", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "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_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.PUB@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_EverCrypt.DRBG.disjoint_st", "equation_EverCrypt.DRBG.footprint", "equation_EverCrypt.DRBG.footprint_s", "equation_EverCrypt.DRBG.freeable", "equation_EverCrypt.DRBG.invariant", "equation_EverCrypt.DRBG.invariant_s", "equation_EverCrypt.DRBG.p", "equation_EverCrypt.DRBG.preserves_freeable", "equation_EverCrypt.DRBG.repr", "equation_EverCrypt.DRBG.state", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_stack_region", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.live_region", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_FStar.Set.subset", "equation_Hacl.HMAC_DRBG.disjoint_st", "equation_Hacl.HMAC_DRBG.footprint", "equation_Hacl.HMAC_DRBG.invariant", "equation_Hacl.HMAC_DRBG.max_additional_input_length", "equation_Hacl.HMAC_DRBG.max_output_length", "equation_Hacl.HMAC_DRBG.repr", "equation_Hacl.Hash.Definitions.hash_len", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.get", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.generate", "equation_Spec.HMAC_DRBG.is_supported_alg", "equation_Spec.HMAC_DRBG.reseed", "equation_Spec.HMAC_DRBG.reseed_interval", "equation_Spec.HMAC_DRBG.supported_alg", "fuel_guarded_inversion_EverCrypt.DRBG.state_s", "fuel_guarded_inversion_Hacl.HMAC_DRBG.state", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.int", "function_token_typing_Spec.AES.elem", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "inversion-interp", "kinding_EverCrypt.DRBG.state_s@tok", "lemma_EverCrypt.DRBG.invert_state_s", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Monotonic.HyperHeap.lemma_extends_includes", "lemma_FStar.Monotonic.HyperHeap.lemma_extends_parent", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Monotonic.HyperStack.lemma_map_invariant", "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors", "lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.lemma_equal_refl", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.uv_inv", "lemma_Lib.IntTypes.gt_lemma", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.live_region_frameOf", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_regions", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_addresses_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.loc_union_loc_none_r", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_live_region", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_region_buffer", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_region_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_region_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_refl", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.region_liveness_insensitive_addresses", "lemma_LowStar.Monotonic.Buffer.region_liveness_insensitive_buffer", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_Negation", "proj_equation_Hacl.HMAC_DRBG.State_k", "proj_equation_Hacl.HMAC_DRBG.State_reseed_counter", "proj_equation_Hacl.HMAC_DRBG.State_v", "proj_equation_Spec.GaloisField.GF_t", "proj_equation_Spec.HMAC_DRBG.State_k", "proj_equation_Spec.HMAC_DRBG.State_reseed_counter", "proj_equation_Spec.HMAC_DRBG.State_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_FStar.Pervasives.Native.Some_a", "projection_inverse_FStar.Pervasives.Native.Some_v", "projection_inverse_Spec.GaloisField.GF_t", "projection_inverse_Spec.HMAC_DRBG.State_k", "projection_inverse_Spec.HMAC_DRBG.State_reseed_counter", "projection_inverse_Spec.HMAC_DRBG.State_v", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_1cc6c9f8558dddb337b6c1187115cd6a", "refinement_interpretation_Tm_refine_2a15b2f3446cd38dd7db324af10b1b71", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4b484af68eae8d74dfeb59bfc788394f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a6333d0062adb26648db1aa8e5e8a193", "refinement_interpretation_Tm_refine_aeb2e4ee46d14b3b648f70c9a5c878c5", "refinement_interpretation_Tm_refine_bd307bf4af18b48116192667829bd5c7", "refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b", "refinement_interpretation_Tm_refine_ca2e1245e92dc19badb6bd4080158f18", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_EverCrypt.DRBG.footprint", "typing_EverCrypt.DRBG.footprint_s", "typing_EverCrypt.DRBG.p", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Map.sel", "typing_FStar.Map.upd", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.includes", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Monotonic.HyperStack.live_region", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.empty", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_Hacl.HMAC_DRBG.__proj__State__item__k", "typing_Hacl.HMAC_DRBG.__proj__State__item__reseed_counter", "typing_Hacl.HMAC_DRBG.__proj__State__item__v", "typing_Hacl.HMAC_DRBG.max_additional_input_length", "typing_Hacl.HMAC_DRBG.max_output_length", "typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar", "typing_Lib.Buffer.union", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.get", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_LowStar.Monotonic.Buffer.region_liveness_insensitive_locs", "typing_Spec.HMAC_DRBG.is_supported_alg", "typing_Spec.HMAC_DRBG.reseed_interval", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "e45b3f775a351ddc015f647bef0f9d59" ], [ "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, "f03b4c4035b1596f311352e8ba590699" ], [ "EverCrypt.DRBG.generate_sha1", 2, 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, "5b49900bb909d5a6ff7c1a8edf94b774" ], [ "EverCrypt.DRBG.generate_sha2_256", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "7e1f965d3b79a4c20a4a01f7bb28e5f1" ], [ "EverCrypt.DRBG.generate_sha2_256", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "9c568a6ad2e4babe6942ff29ff1e26a7" ], [ "EverCrypt.DRBG.generate_sha2_384", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "3b6d13e38c3ab0395706a8ef2e4e3e58" ], [ "EverCrypt.DRBG.generate_sha2_384", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "0d5ce16551e733b31f64839dfa356fa5" ], [ "EverCrypt.DRBG.generate_sha2_512", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_FStar.Integers.W32@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "1f9c14c25ce176d2cc1fa362a3464b5d" ], [ "EverCrypt.DRBG.generate_sha2_512", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_FStar.Integers.W32@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "163acfd49982f16ef93e2bfb9347cb93" ], [ "EverCrypt.DRBG.mk_uninstantiate", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_typing", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W64", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "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", "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_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", "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.DRBG.footprint", "equation_EverCrypt.DRBG.footprint_s", "equation_EverCrypt.DRBG.freeable", "equation_EverCrypt.DRBG.freeable_s", "equation_EverCrypt.DRBG.invariant", "equation_EverCrypt.DRBG.invariant_s", "equation_EverCrypt.DRBG.state", "equation_EverCrypt.Helpers.uint32_t", "equation_FStar.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.equal_stack_domains", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.mem", "equation_Hacl.HMAC_DRBG.footprint", "equation_Hacl.HMAC_DRBG.freeable", "equation_Hacl.HMAC_DRBG.invariant", "equation_Hacl.Hash.Definitions.hash_len", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.pointer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.disjoint", "equation_LowStar.Monotonic.Buffer.length", "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.hash_length", "equation_Spec.Hash.Definitions.hash_word_length", "equation_Spec.Hash.Definitions.word_length", "fuel_guarded_inversion_EverCrypt.DRBG.state_s", "fuel_guarded_inversion_Hacl.HMAC_DRBG.state", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.size_t", "function_token_typing_LowStar.Buffer.trivial_preorder", "function_token_typing_Prims.int", "function_token_typing_Spec.AES.elem", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "inversion-interp", "kinding_EverCrypt.DRBG.state_s@tok", "l_and-interp", "lemma_EverCrypt.DRBG.invert_state_s", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_stack_regions_intro", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.UInt32.uv_inv", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.freeable_disjoint_", "lemma_LowStar.Monotonic.Buffer.freeable_length", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_Multiply", "proj_equation_Hacl.HMAC_DRBG.State_k", "proj_equation_Hacl.HMAC_DRBG.State_reseed_counter", "proj_equation_Hacl.HMAC_DRBG.State_v", "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_011fc5e09a4acad66368a3ceedbeb477", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0aa1fb4cf1fd7b03d18656467483972c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4b484af68eae8d74dfeb59bfc788394f", "refinement_interpretation_Tm_refine_4ed8a4298bca8cb352250b969ab88fcc", "refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e", "refinement_interpretation_Tm_refine_6e699e31311662dc04cc2225427500fa", "refinement_interpretation_Tm_refine_6fe0e60357bf11b7e5a0634013389eb0", "refinement_interpretation_Tm_refine_822d47def75b4fb1f118e901cb4a38d6", "refinement_interpretation_Tm_refine_979c5307d753ef716d26dee1ee39c904", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_ef676f9ab92641194f8458f703a0b54d", "refinement_interpretation_Tm_refine_f1a8e39e84b3b2c503c7dd7280929634", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "true_interp", "typing_EverCrypt.DRBG.footprint", "typing_EverCrypt.DRBG.footprint_s", "typing_EverCrypt.DRBG.p", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Set.singleton", "typing_FStar.UInt32.t", "typing_Hacl.HMAC_DRBG.__proj__State__item__k", "typing_Hacl.HMAC_DRBG.__proj__State__item__reseed_counter", "typing_Hacl.HMAC_DRBG.__proj__State__item__v", "typing_Hacl.Hash.Definitions.hash_len", "typing_Lib.Buffer.loc", "typing_Lib.Buffer.union", "typing_Lib.IntTypes.unsigned", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Hash.Definitions.hash_length", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "9de70ba7135b7612e6da030a41050d83" ], [ "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, "a2aacaffaa9623754864bc1a92f9adbe" ], [ "EverCrypt.DRBG.uninstantiate_sha1", 2, 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, "5d2a2bd733432a0b6d710333980a8562" ], [ "EverCrypt.DRBG.uninstantiate_sha2_256", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "91fe5449d1b10813839390f82374ad27" ], [ "EverCrypt.DRBG.uninstantiate_sha2_256", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "96b1a92db8868ccfed92812a243925cb" ], [ "EverCrypt.DRBG.uninstantiate_sha2_384", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "0e78d879c2ae53a3570b9e9bf390d750" ], [ "EverCrypt.DRBG.uninstantiate_sha2_384", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "equality_tok_FStar.Integers.W16@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "218816f0ab876130ada3e460150baecd" ], [ "EverCrypt.DRBG.uninstantiate_sha2_512", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_FStar.Integers.W32@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "cc4dff23cbb27abdbb6150ae4eed42a0" ], [ "EverCrypt.DRBG.uninstantiate_sha2_512", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Hash.Definitions.SHA2_512", "equality_tok_FStar.Integers.W32@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Hash.Definitions.SHA2_512@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.HMAC_DRBG.is_supported_alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_FStar.Integers.Unsigned__0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "c67ad4155e2cd4014aa812b394e29e8b" ], [ "EverCrypt.DRBG.instantiate", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Spec.Hash.Definitions.SHA1", "data_elim_EverCrypt.DRBG.SHA1_s", "data_elim_EverCrypt.DRBG.SHA2_256_s", "data_elim_EverCrypt.DRBG.SHA2_384_s", "data_elim_EverCrypt.DRBG.SHA2_512_s", "disc_equation_EverCrypt.DRBG.SHA1_s", "disc_equation_EverCrypt.DRBG.SHA2_256_s", "disc_equation_EverCrypt.DRBG.SHA2_384_s", "disc_equation_EverCrypt.DRBG.SHA2_512_s", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_EverCrypt.DRBG.invariant", "equation_Spec.HMAC_DRBG.min_length", "equation_Spec.HMAC_DRBG.supported_alg", "fuel_guarded_inversion_EverCrypt.DRBG.state_s", "inversion-interp", "lemma_EverCrypt.DRBG.invert_state_s", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_1ec3ac28925f79ae919d8cb783df7510", "refinement_interpretation_Tm_refine_66c445b2fcabfccf8b428a12281d19e4", "refinement_interpretation_Tm_refine_690de812cb004d8deefd3e94ad4e06d5", "refinement_interpretation_Tm_refine_8260ad71529a2f4ea650740ff4f49c6b", "refinement_interpretation_Tm_refine_c29da4dc404f1e03a0ee001fd54775e1", "refinement_kinding_Tm_refine_822d47def75b4fb1f118e901cb4a38d6", "typing_FStar.Ghost.reveal" ], 0, "9550553eb31da35119b55f322721fede" ], [ "EverCrypt.DRBG.reseed", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Spec.Hash.Definitions.SHA1", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "constructor_distinct_Spec.Hash.Definitions.SHA2_384", "constructor_distinct_Tm_unit", "data_elim_EverCrypt.DRBG.SHA1_s", "data_elim_EverCrypt.DRBG.SHA2_256_s", "data_elim_EverCrypt.DRBG.SHA2_384_s", "data_elim_EverCrypt.DRBG.SHA2_512_s", "disc_equation_EverCrypt.DRBG.SHA1_s", "disc_equation_EverCrypt.DRBG.SHA2_256_s", "disc_equation_EverCrypt.DRBG.SHA2_384_s", "disc_equation_EverCrypt.DRBG.SHA2_512_s", "equality_tok_FStar.Integers.W16@tok", "equality_tok_FStar.Integers.W8@tok", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_384@tok", "equation_EverCrypt.DRBG.invariant", "equation_EverCrypt.DRBG.p", "equation_Spec.HMAC_DRBG.min_length", "equation_Spec.HMAC_DRBG.supported_alg", "fuel_guarded_inversion_EverCrypt.DRBG.state_s", "fuel_guarded_inversion_Hacl.HMAC_DRBG.state", "inversion-interp", "lemma_EverCrypt.DRBG.invert_state_s", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Integers.Signed__0", "projection_inverse_FStar.Integers.Unsigned__0", "refinement_interpretation_Tm_refine_1ec3ac28925f79ae919d8cb783df7510", "refinement_interpretation_Tm_refine_66c445b2fcabfccf8b428a12281d19e4", "refinement_interpretation_Tm_refine_690de812cb004d8deefd3e94ad4e06d5", "refinement_interpretation_Tm_refine_8260ad71529a2f4ea650740ff4f49c6b", "refinement_interpretation_Tm_refine_c29da4dc404f1e03a0ee001fd54775e1", "refinement_kinding_Tm_refine_822d47def75b4fb1f118e901cb4a38d6", "typing_EverCrypt.DRBG.p", "typing_FStar.Ghost.reveal" ], 0, "e70cc362086750c8c739f6e9899e99ca" ], [ "EverCrypt.DRBG.generate", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Spec.Hash.Definitions.SHA1", "data_elim_EverCrypt.DRBG.SHA1_s", "data_elim_EverCrypt.DRBG.SHA2_256_s", "data_elim_EverCrypt.DRBG.SHA2_384_s", "data_elim_EverCrypt.DRBG.SHA2_512_s", "disc_equation_EverCrypt.DRBG.SHA1_s", "disc_equation_EverCrypt.DRBG.SHA2_256_s", "disc_equation_EverCrypt.DRBG.SHA2_384_s", "disc_equation_EverCrypt.DRBG.SHA2_512_s", "equality_tok_Spec.Hash.Definitions.SHA1@tok", "equation_EverCrypt.DRBG.invariant", "equation_Spec.HMAC_DRBG.min_length", "equation_Spec.HMAC_DRBG.supported_alg", "fuel_guarded_inversion_EverCrypt.DRBG.state_s", "inversion-interp", "lemma_EverCrypt.DRBG.invert_state_s", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_22d78f976845170c04c3972ddc9b2b6a", "refinement_interpretation_Tm_refine_62ecfe7734aa686be207e777be796d32", "refinement_interpretation_Tm_refine_7d03d84e8e52886fa53697dae444c35c", "refinement_interpretation_Tm_refine_abe75a70d46d4140a5fea50c7c91210c", "refinement_interpretation_Tm_refine_fb83f12a2fa502578e76817c10c7cedd", "refinement_kinding_Tm_refine_822d47def75b4fb1f118e901cb4a38d6", "typing_FStar.Ghost.reveal" ], 0, "13afcc55c99f249e0c45069e13679ad7" ], [ "EverCrypt.DRBG.uninstantiate", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "data_elim_EverCrypt.DRBG.SHA1_s", "data_elim_EverCrypt.DRBG.SHA2_256_s", "data_elim_EverCrypt.DRBG.SHA2_384_s", "data_elim_EverCrypt.DRBG.SHA2_512_s", "disc_equation_EverCrypt.DRBG.SHA1_s", "disc_equation_EverCrypt.DRBG.SHA2_256_s", "disc_equation_EverCrypt.DRBG.SHA2_384_s", "disc_equation_EverCrypt.DRBG.SHA2_512_s", "equation_EverCrypt.DRBG.invariant", "equation_Spec.HMAC_DRBG.supported_alg", "fuel_guarded_inversion_EverCrypt.DRBG.state_s", "inversion-interp", "lemma_EverCrypt.DRBG.invert_state_s", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_Tm_refine_7fa36a4edd1e7239da6bbb9ddec2c550", "refinement_interpretation_Tm_refine_99ac42ec998fe0642243f2353af4704b", "refinement_interpretation_Tm_refine_bc8a2548296a27ae805ddb83e27425e4", "refinement_interpretation_Tm_refine_d9cc78ecd051d9ff734f205819138c3c", "refinement_interpretation_Tm_refine_feb1ba767799040a4093b9851d047f11", "refinement_kinding_Tm_refine_822d47def75b4fb1f118e901cb4a38d6", "typing_FStar.Ghost.reveal" ], 0, "e3ba62da611a65c7a55a0e7dd7233a0b" ] ] ]