Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC
OCaml API: Don't run unit tests which require unsupported features
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,
"80378365a7c04a915a77cb87b1263401"
],
[
"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,
"4380d84edac76b174bfc3a4b007fefb2"
],
[
"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,
"40d8f95b22728704b1251df717563dc1"
],
[
"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,
"26f90d7413a884d77a27829cd722a7d1"
],
[
"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,
"657c1bf6a889dc1d911755da6fd2f5d3"
],
[
"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,
"e2f6c1ba03efb7a4bcdcda55bd2180a2"
],
[
"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,
"a4e6510fbc1ba28b4e0c09cce7ba6c7c"
],
[
"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,
"d8b085d148120a545c14f0a756f32516"
],
[
"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,
"0b4e95e876dfc737e6c63b10f40ef0e8"
],
[
"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,
"bda8692f68bdd0d612850b8113ab787c"
],
[
"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,
"05a0b1a114df4c09d09c568b8b23a462"
],
[
"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,
"c8daf3138af129b3ddce921829b9fcbc"
],
[
"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,
"c7828a5e8a81a51f85b853060aeca2d7"
],
[
"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,
"da82686f46d5f2163ccafd198ca26e7a"
],
[
"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,
"a3d12a879bb8479fa413cf4b3b899b0a"
],
[
"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,
"a710ea3bec6f640159265ab876361f02"
],
[
"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,
"59d35a12338892f731f98a0cdb792279"
],
[
"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,
"9c5786a0c759be6bc39dbb211a0adb99"
]
]
]
Computing file changes ...
