Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
EverCrypt.DRBG.fst.hints
[
"��\u0001��;�^�\u000bN��\u00069�",
[
[
"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,
"ac4021b739a6ad9d2923a94bd5d2afe2"
],
[
"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,
"a9c893b614d0a6791354662e2ec4487a"
],
[
"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,
"20542794f0fdca3c71b22d43824e1617"
],
[
"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,
"ea5acfc670f000d33269d6b4d6b3deab"
],
[
"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,
"843f5ccc6b756b1f133122ffa985c97e"
],
[
"EverCrypt.DRBG.min_length",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U32",
"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.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned",
"equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.HMAC_DRBG.min_length",
"equation_Spec.HMAC_DRBG.supported_alg",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"typing_Spec.Agile.HMAC.is_supported_alg"
],
0,
"fc9e047098c50e64e9e16368c84d75a9"
],
[
"EverCrypt.DRBG.state_s",
1,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"20c3fee313e52be9b0e04959f8434fdb"
],
[
"EverCrypt.DRBG.state_s",
2,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"899a6c8b04599777704a06fa18f2f223"
],
[
"EverCrypt.DRBG.state_s",
3,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"85e154a3e25bb93680181bd1523fef12"
],
[
"EverCrypt.DRBG.state_s",
4,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"b564047bfe1ad6eb6a95d6bdf6a6a4bd"
],
[
"EverCrypt.DRBG.state_s",
5,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"f1634baa33d82055f6df385d666b48d1"
],
[
"EverCrypt.DRBG.state_s",
6,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"56579b842105f72f8f4fc8d2985faebf"
],
[
"EverCrypt.DRBG.state_s",
7,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"7a3e640c703fdfdd1098f1bd545aa820"
],
[
"EverCrypt.DRBG.state_s",
8,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"921a818462c38ea628ee48f1b1130dec"
],
[
"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.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"29c890368455f7a9279c736c9befb76a"
],
[
"EverCrypt.DRBG.__proj__SHA1_s__item___0",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"disc_equation_EverCrypt.DRBG.SHA1_s",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_0e97eceb5a4fa3473c9281e4e259d6ff"
],
0,
"d199a6c743a392f37118f6c70be77110"
],
[
"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.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_31cbfb78bf9a2736dec227846252ef73"
],
0,
"8f6ec3133e4247f4338c82ffa0ddf01d"
],
[
"EverCrypt.DRBG.__proj__SHA2_256_s__item___0",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"disc_equation_EverCrypt.DRBG.SHA2_256_s",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Agile.HMAC.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,
"186d93100140243fe6c0968a3a8f0d52"
],
[
"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.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_48725dc4965c47559da6abe7dbe84cfb"
],
0,
"db99191158a59bb04efd1ca48f194057"
],
[
"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.Agile.HMAC.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,
"8be1ee4c60c66595b45fcfa5a8ce1702"
],
[
"EverCrypt.DRBG.__proj__SHA2_512_s__item___0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"disc_equation_EverCrypt.DRBG.SHA2_512_s",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_c51a2c9d00ea095bc4546df321dd3dae"
],
0,
"6953fec63a1e67253d85163ff8b2ca91"
],
[
"EverCrypt.DRBG.__proj__SHA2_512_s__item___0",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"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.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Spec.Agile.HMAC.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,
"ba59eeda6335b71eeb4d62db025cc1ed"
],
[
"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,
"420c37dd79f99ffb96e981a64b2ccb7f"
],
[
"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,
"df1437abecaeed755e7df853388c1329"
],
[
"EverCrypt.DRBG.loc_includes_union_l_footprint_s",
1,
0,
0,
[ "@query" ],
0,
"b82dd879c72665c81854be532938ee63"
],
[
"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,
"f5626a2b08271b40002eefc2f5e31a1e"
],
[
"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,
"502df9341b5dd9740812f64959e7da15"
],
[
"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.W31",
"constructor_distinct_FStar.Integers.W32",
"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",
"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.W31@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_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.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.size_t", "equation_Lib.IntTypes.uint8",
"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.Agile.HMAC.is_supported_alg",
"equation_Spec.HMAC_DRBG.supported_alg",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt32.t",
"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.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",
"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",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"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_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"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_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_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.length",
"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.Agile.HMAC.is_supported_alg",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"cb08995adb880712514e76ec7e473a6c"
],
[
"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.W31",
"constructor_distinct_FStar.Integers.W32",
"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",
"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",
"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.W31@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_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.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.fresh_loc",
"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_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.UInt32.t",
"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", "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",
"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",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"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_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_EverCrypt.DRBG.footprint_s", "typing_EverCrypt.DRBG.p",
"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_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_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.length",
"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.Agile.HMAC.is_supported_alg",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"eaa882381d3b368e5bab9be67e61fe7c"
],
[
"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,
"58197a62b371a0f450c65ee9e8c4b835"
],
[
"EverCrypt.DRBG.instantiate_st",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W8",
"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.W31@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_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.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.HMAC_DRBG.max_length",
"equation_Spec.HMAC_DRBG.max_personalization_string_length",
"equation_Spec.HMAC_DRBG.min_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_word_length",
"equation_Spec.Hash.Definitions.word_length",
"fuel_guarded_inversion_EverCrypt.DRBG.state_s",
"fuel_guarded_inversion_Spec.HMAC_DRBG.state",
"function_token_typing_Lib.IntTypes.uint8", "int_typing",
"inversion-interp", "kinding_EverCrypt.DRBG.state_s@tok",
"lemma_EverCrypt.DRBG.invert_state_s",
"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_Negation", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_ca2e1245e92dc19badb6bd4080158f18",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.get",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Spec.Agile.HMAC.is_supported_alg",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"0eb1126da32c60f01c9372fa10c1b8f8"
],
[
"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.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.S128",
"constructor_distinct_Lib.IntTypes.U1",
"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.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_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_14aab2321e74365959b67105c3406f1a",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"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_c6c18a7ceb46d419c35ff8551117551e",
"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,
"1c7f51168c6cbabd7604c1d57cb8e210"
],
[
"EverCrypt.DRBG.instantiate_sha1",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"1f80ab872fdb9fb82c77f2e470bbe131"
],
[
"EverCrypt.DRBG.instantiate_sha1",
2,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"27afcb8a7a42b635922dbf41c98766a6"
],
[
"EverCrypt.DRBG.instantiate_sha2_256",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"360bc2d7e57ab2c730f5b553359b47a3"
],
[
"EverCrypt.DRBG.instantiate_sha2_256",
2,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"ef61bba394e23ff1335d52b79afef88a"
],
[
"EverCrypt.DRBG.instantiate_sha2_384",
1,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"6ecf39ec58fd1a1b9628d1662a480fa6"
],
[
"EverCrypt.DRBG.instantiate_sha2_384",
2,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"1e018ad6c303c6dd286a4588df426974"
],
[
"EverCrypt.DRBG.instantiate_sha2_512",
1,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"6937c6feeea8c9f1d60d97d952894c5e"
],
[
"EverCrypt.DRBG.instantiate_sha2_512",
2,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"fb84dbb58a0370b4f3990ba166848456"
],
[
"EverCrypt.DRBG.reseed_st",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W8",
"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.W31@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_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.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.HMAC_DRBG.max_additional_input_length",
"equation_Spec.HMAC_DRBG.max_length",
"equation_Spec.HMAC_DRBG.min_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_word_length",
"equation_Spec.Hash.Definitions.word_length",
"fuel_guarded_inversion_EverCrypt.DRBG.state_s",
"fuel_guarded_inversion_Spec.HMAC_DRBG.state",
"function_token_typing_Lib.IntTypes.uint8", "int_typing",
"inversion-interp", "kinding_EverCrypt.DRBG.state_s@tok",
"lemma_EverCrypt.DRBG.invert_state_s",
"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_Negation", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_ca2e1245e92dc19badb6bd4080158f18",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.get",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Spec.Agile.HMAC.is_supported_alg",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"358038dc92f64d51bd8bcd5ab7b959cd"
],
[
"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,
"c4f81a58c2ee92f53ad16053fcfcf5e7"
],
[
"EverCrypt.DRBG.reseed_sha1",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"30e7678a1ac96dcfa46b8ef2713102ed"
],
[
"EverCrypt.DRBG.reseed_sha1",
2,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"780f30fc5e0e2f6f65f2e71b011c8391"
],
[
"EverCrypt.DRBG.reseed_sha2_256",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"68f832127508bad3f2e1815bd52f940e"
],
[
"EverCrypt.DRBG.reseed_sha2_256",
2,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"b6985845ca958333fa0a1d595aa24154"
],
[
"EverCrypt.DRBG.reseed_sha2_384",
1,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"bbb6a5213524d4b7a137a4b380399f64"
],
[
"EverCrypt.DRBG.reseed_sha2_384",
2,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"fe80728e200ab5a857c76de653a871dd"
],
[
"EverCrypt.DRBG.reseed_sha2_512",
1,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"15832ec763ea6e29d706046001b04e71"
],
[
"EverCrypt.DRBG.reseed_sha2_512",
2,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"eb47bc11e13fe35858e0c14d334423a3"
],
[
"EverCrypt.DRBG.generate_st",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Pervasives.Native.Some",
"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",
"disc_equation_FStar.Pervasives.Native.Some",
"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.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_EverCrypt.DRBG.state", "equation_Lib.IntTypes.bits",
"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.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.HMAC_DRBG.generate",
"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.min_length",
"equation_Spec.HMAC_DRBG.reseed",
"equation_Spec.HMAC_DRBG.reseed_interval",
"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.hash_word_length",
"equation_Spec.Hash.Definitions.word_length",
"fuel_guarded_inversion_EverCrypt.DRBG.state_s",
"fuel_guarded_inversion_Spec.HMAC_DRBG.state",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "inversion-interp",
"kinding_EverCrypt.DRBG.state_s@tok",
"lemma_EverCrypt.DRBG.invert_state_s",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
"proj_equation_Spec.HMAC_DRBG.State_reseed_counter",
"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.HMAC_DRBG.State_reseed_counter",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_aeb2e4ee46d14b3b648f70c9a5c878c5",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.get",
"typing_LowStar.Monotonic.Buffer.len",
"typing_Spec.Agile.HMAC.is_supported_alg",
"typing_Spec.HMAC_DRBG.reseed_interval",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"a5aca03acbda617ed7002574db538559"
],
[
"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.W31",
"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.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",
"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_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.minint", "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.disjoint",
"equation_LowStar.Monotonic.Buffer.get",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.HMAC_DRBG.generate", "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",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"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.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.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_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_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_a6333d0062adb26648db1aa8e5e8a193",
"refinement_interpretation_Tm_refine_aeb2e4ee46d14b3b648f70c9a5c878c5",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde",
"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_output_length",
"typing_Hacl.Hash.Definitions.hash_len", "typing_Lib.Buffer.loc",
"typing_Lib.Buffer.op_Bar_Plus_Bar", "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_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.Agile.HMAC.is_supported_alg",
"typing_Spec.HMAC_DRBG.reseed_interval",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"10883f208ab177d6635f263a0b7b77ef"
],
[
"EverCrypt.DRBG.generate_sha1",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"98096f51bb3c18c79dd425243c5dcca8"
],
[
"EverCrypt.DRBG.generate_sha1",
2,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"e9ad3d22e1ab87187fb6637a3d3dbd96"
],
[
"EverCrypt.DRBG.generate_sha2_256",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"d89782d1908dde1f13f98edd85e99b96"
],
[
"EverCrypt.DRBG.generate_sha2_256",
2,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"48cd121840347a526be11243bce1f2ac"
],
[
"EverCrypt.DRBG.generate_sha2_384",
1,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"9840a9bf60c0fcc39633f352a1c99304"
],
[
"EverCrypt.DRBG.generate_sha2_384",
2,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"38d48508bedcb145ffe630dcd52e221e"
],
[
"EverCrypt.DRBG.generate_sha2_512",
1,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"080144939004f101cbde7cc36f72f128"
],
[
"EverCrypt.DRBG.generate_sha2_512",
2,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"6e5d282b88e4d3273e486e98d37079f8"
],
[
"EverCrypt.DRBG.mk_uninstantiate",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"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",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@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_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_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_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.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.modifies",
"equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
"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.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.disjoint",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Agile.HMAC.is_supported_alg",
"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_Lib.IntTypes.uint8",
"function_token_typing_LowStar.Buffer.trivial_preorder",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
"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_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"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.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"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_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "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",
"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_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_011fc5e09a4acad66368a3ceedbeb477",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0fcc22fcb88830a6c8dcc507be39a596",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4b484af68eae8d74dfeb59bfc788394f",
"refinement_interpretation_Tm_refine_4ed8a4298bca8cb352250b969ab88fcc",
"refinement_interpretation_Tm_refine_573cfed777dae20cc82e8fef9622857e",
"refinement_interpretation_Tm_refine_6fe0e60357bf11b7e5a0634013389eb0",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_979c5307d753ef716d26dee1ee39c904",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_c7753baa38cd99c4f00a675631dc1dde",
"refinement_interpretation_Tm_refine_ef676f9ab92641194f8458f703a0b54d",
"refinement_interpretation_Tm_refine_f01dc0d0a678a9d1eefaecf764af2f37",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"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_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.v",
"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.Agile.HMAC.is_supported_alg",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"d383ea2d87891feeda63c5ef64bc9590"
],
[
"EverCrypt.DRBG.uninstantiate_sha1",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"75ccf20a8b830ee91da67c822b174b7f"
],
[
"EverCrypt.DRBG.uninstantiate_sha1",
2,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_Spec.Hash.Definitions.SHA1@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"4d8e20f3c61d48d50a7f625e87c9fe10"
],
[
"EverCrypt.DRBG.uninstantiate_sha2_256",
1,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"38c92095822dcdc21bec9091da889520"
],
[
"EverCrypt.DRBG.uninstantiate_sha2_256",
2,
0,
0,
[
"@query", "constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0"
],
0,
"bd21949a126d5d14049494964fea2d52"
],
[
"EverCrypt.DRBG.uninstantiate_sha2_384",
1,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"e1c3ecf426456f0bdf4cc0936ca806ec"
],
[
"EverCrypt.DRBG.uninstantiate_sha2_384",
2,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_Spec.Hash.Definitions.SHA2_384",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_384@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"1de7d30a43e1f098fee9b44e4ad16218"
],
[
"EverCrypt.DRBG.uninstantiate_sha2_512",
1,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"93d8e10d5ced56bc50fddbae363b21a1"
],
[
"EverCrypt.DRBG.uninstantiate_sha2_512",
2,
0,
0,
[
"@query", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Spec.Agile.HMAC.is_supported_alg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0"
],
0,
"e0e81adfbec0259d58a346b0a881e012"
],
[
"EverCrypt.DRBG.instantiate",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"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.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_EverCrypt.DRBG.invariant", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length",
"equation_Spec.HMAC_DRBG.supported_alg",
"fuel_guarded_inversion_EverCrypt.DRBG.state_s",
"function_token_typing_Lib.IntTypes.uint8", "inversion-interp",
"lemma_EverCrypt.DRBG.invert_state_s", "lemma_FStar.UInt32.uv_inv",
"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_00b7086f5544e6080b4b49859916f574",
"typing_FStar.Ghost.reveal",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len"
],
0,
"605b2076f7b3774c7fa6f512de22f8b1"
],
[
"EverCrypt.DRBG.reseed",
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",
"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_00b7086f5544e6080b4b49859916f574",
"typing_FStar.Ghost.reveal"
],
0,
"86223866e177169add0c2a12147d8298"
],
[
"EverCrypt.DRBG.generate",
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",
"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_00b7086f5544e6080b4b49859916f574",
"typing_FStar.Ghost.reveal"
],
0,
"14f6cd68d1ca9e61d791dbd7b938855a"
],
[
"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",
"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_00b7086f5544e6080b4b49859916f574",
"typing_FStar.Ghost.reveal"
],
0,
"1d017834e99a4de1d3d363fcf1e06869"
]
]
]
Computing file changes ...
