Revision 724d1045f60f13d79df1afc5190955afdfa73ec1 authored by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC, committed by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC
Co-authored-by: @protz
1 parent ca37fbf
Spec.HMAC_DRBG.fst.hints
[
"���Q�\u001f\u0003v,q\u0006�O���",
[
[
"Spec.HMAC_DRBG.min_length",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"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",
"equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.HMAC_DRBG.supported_alg",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"typing_Spec.Agile.HMAC.is_supported_alg"
],
0,
"dd8536a9ff738c905f9c1f652176ba5c"
],
[
"Spec.HMAC_DRBG.state",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "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", "int_inversion",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"432fb5dedc1efd85991b44df5e7f3150"
],
[
"Spec.HMAC_DRBG.__proj__State__item__k",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "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_Spec.HMAC_DRBG.state", "int_inversion",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"2aa11f41acf77b6a1a88efb04f4249a9"
],
[
"Spec.HMAC_DRBG.__proj__State__item__k",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "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_Spec.HMAC_DRBG.state", "int_inversion",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"21aca360429f56942ffe6dc7bef10608"
],
[
"Spec.HMAC_DRBG.__proj__State__item__v",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "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_Spec.HMAC_DRBG.state", "int_inversion",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"614e54b3566f38ef2eb425c5130be571"
],
[
"Spec.HMAC_DRBG.__proj__State__item__v",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "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_Spec.HMAC_DRBG.state", "int_inversion",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"472f1adad969a47617aa3f905f113c1c"
],
[
"Spec.HMAC_DRBG.hmac_input_bound",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"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",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"typing_Spec.Agile.HMAC.is_supported_alg"
],
0,
"5fd4193777d3d63e708ed2a72e2eba06"
],
[
"Spec.HMAC_DRBG.update",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "equation_Lib.IntTypes.uint8",
"equation_Prims.nat", "equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.Agile.HMAC.lbytes",
"equation_Spec.HMAC_DRBG.supported_alg",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Seq.Base.length",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"92588ef4aa0994278830c833ab156e89"
],
[
"Spec.HMAC_DRBG.update",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "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", "int_inversion",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"d499bdcfb3f897d2bc8bcd00dfad2b77"
],
[
"Spec.HMAC_DRBG.update",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U8@tok",
"equation_FStar.Seq.Base.op_At_Bar",
"equation_FStar.Seq.Properties.cons", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.Agile.HMAC.keysized",
"equation_Spec.Agile.HMAC.lbytes",
"equation_Spec.HMAC_DRBG.supported_alg",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_27dc038cce58e6a175dcb6195f80808a",
"refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_64007e4a8c187c3787ce4f8705e9db35",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_Spec.Hash.Definitions.hash_word_length",
"typing_Spec.Hash.Definitions.word_length",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"710e67b4ac10a0d3c6c089834624b786"
],
[
"Spec.HMAC_DRBG.instantiate",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_FStar.Seq.Base.op_At_Bar", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.HMAC_DRBG.supported_alg",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_27dc038cce58e6a175dcb6195f80808a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_64007e4a8c187c3787ce4f8705e9db35",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_Spec.Hash.Definitions.hash_word_length",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"129d1ca785bbdec9b9d2cd206b081b73"
],
[
"Spec.HMAC_DRBG.reseed",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "equation_FStar.Seq.Base.op_At_Bar",
"equation_Lib.IntTypes.uint8", "equation_Prims.nat",
"equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.HMAC_DRBG.supported_alg",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.word_length",
"fuel_guarded_inversion_Spec.HMAC_DRBG.state",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Seq.Base.length",
"typing_Spec.Hash.Definitions.hash_word_length"
],
0,
"6cba75b371db184c047089e474054546"
],
[
"Spec.HMAC_DRBG.a_spec",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.word_length", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits",
"typing_Spec.Hash.Definitions.hash_word_length",
"typing_Spec.Hash.Definitions.word_length",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"ddf2999fb4faa7f37a2af1a275026708"
],
[
"Spec.HMAC_DRBG.generate_loop",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.Agile.HMAC.lbytes",
"equation_Spec.HMAC_DRBG.supported_alg",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Spec.Hash.Definitions.word_length",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"f9b1f1b6adf2419cc0ba6a611f12da07"
],
[
"Spec.HMAC_DRBG.generate_loop",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "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", "int_inversion",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"a216347e314d668a5fb7a9beee0eda58"
],
[
"Spec.HMAC_DRBG.generate_loop",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit", "equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.Agile.HMAC.keysized",
"equation_Spec.Agile.HMAC.lbytes", "equation_Spec.HMAC_DRBG.a_spec",
"equation_Spec.HMAC_DRBG.supported_alg",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length", "typing_Prims.pow2",
"typing_Spec.Hash.Definitions.hash_word_length",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"1110a9836c476db25c2bd3eed8af39b2"
],
[
"Spec.HMAC_DRBG.generate",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_FStar.Seq.Base.op_At_Bar", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.Agile.HMAC.keysized",
"equation_Spec.Agile.HMAC.lbytes", "equation_Spec.HMAC_DRBG.a_spec",
"equation_Spec.HMAC_DRBG.max_output_length",
"equation_Spec.HMAC_DRBG.supported_alg",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.word_length",
"fuel_guarded_inversion_Spec.HMAC_DRBG.state",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"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.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_56c56f560459dc6c90e1044e54e31f27",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8839f8ed7b036627b162519c87dcea66",
"refinement_interpretation_Tm_refine_a8645f2c9391f0b1eef5cf29231f10dd",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
"typing_Lib.Sequence.length", "typing_Lib.Sequence.to_seq",
"typing_Spec.Agile.HMAC.is_supported_alg",
"typing_Spec.HMAC_DRBG.__proj__State__item__k",
"typing_Spec.HMAC_DRBG.__proj__State__item__reseed_counter",
"typing_Spec.HMAC_DRBG.__proj__State__item__v",
"typing_Spec.Hash.Definitions.word_length",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"94bba4ae3f14fb85a13ce81650bd31f4"
],
[
"Spec.HMAC_DRBG.generate'",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Spec.Agile.HMAC.is_supported_alg",
"equation_Spec.HMAC_DRBG.max_output_length",
"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_Spec.HMAC_DRBG.state",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.HMAC_DRBG.State_reseed_counter",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_00b7086f5544e6080b4b49859916f574",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5ecded4928a77b5c9da75dea0bcdc683",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_Lib.IntTypes.minint",
"typing_Spec.Agile.HMAC.is_supported_alg",
"typing_Spec.HMAC_DRBG.__proj__State__item__reseed_counter",
"typing_Spec.Hash.Definitions.word_length",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"5ecd36154e1fa5687054038dd50a661a"
]
]
]
Computing file changes ...
