Revision 1539fc67ec7cd1f092967452d8ae47d170ca149b authored by Jonathan Protzenko on 24 April 2020, 23:18:32 UTC, committed by Jonathan Protzenko on 24 April 2020, 23:18:32 UTC
1 parent 56130dc
Spec.HKDF.fst.hints
[
"\u0011'Թ+�Y��Cq�\t�GI",
[
[
"Spec.HKDF.extract",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"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.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"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.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.HMAC.keysized",
"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.Hash.Definitions.hash_alg",
"function_token_typing_Lib.IntTypes.uint8", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_93a6f01b8db682f6bc12e718db5c8201",
"typing_FStar.Seq.Base.length"
],
0,
"c5325ed682b8bcf65b01781512fdacd6"
],
[
"Spec.HKDF.extract",
2,
2,
1,
[ "@query" ],
0,
"24faccbe47cc660de0177d6048f288b1"
],
[
"Spec.HKDF.expand0",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Spec.Hash.Definitions_pretyping_332103d8b337802efb5758d608edf05f",
"constructor_distinct_FStar.Integers.Signed",
"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_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"constructor_distinct_Tm_unit",
"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_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equation_FStar.Integers.int_t", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype",
"equation_Prims.nat", "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.max_input_length",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5fd6c3de1f973b05a3cba6286941107c",
"refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955",
"typing_Spec.Hash.Definitions.hash_word_length",
"typing_Spec.Hash.Definitions.max_input_length",
"typing_Spec.Hash.Definitions.word_length",
"typing_tok_Spec.Hash.Definitions.SHA2_224@tok"
],
0,
"e62170e4f0b1a6542b92cccaca178c27"
],
[
"Spec.HKDF.expand0",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Spec.Hash.Definitions_pretyping_332103d8b337802efb5758d608edf05f",
"binder_x_0335d097736105e3c47c453b75a97e40_5",
"binder_x_332103d8b337802efb5758d608edf05f_0",
"binder_x_8f7f11c8feab2d1dbfb8e60676b43aaf_3",
"binder_x_8f7f11c8feab2d1dbfb8e60676b43aaf_4",
"binder_x_c230bc14f5b76230f719e4273030cc0c_2",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_224@tok",
"equation_FStar.Integers.int_t",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Seq.Base.op_At_Bar",
"equation_FStar.Seq.Properties.split", "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.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Spec.HMAC.lbytes",
"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",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"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.Mktuple2__1",
"refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7fbc3ed0f4b648e90ce1b1b7f0866021",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_e72e2fe2030ad7cd34f9fed5f56bf0da",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.maxint", "typing_Lib.IntTypes.minint",
"typing_Spec.Hash.Definitions.hash_word_length",
"typing_Spec.Hash.Definitions.word_length",
"typing_tok_Lib.IntTypes.U8@tok",
"typing_tok_Spec.Hash.Definitions.SHA2_224@tok",
"well-founded-ordering-on-nat"
],
0,
"e75374ff1dafca770819f392fa8c1382"
],
[
"Spec.HKDF.expand0",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint8",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.bytes",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_1d9166622f9d5c9d61386ed36d354fbf",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Seq.Base.length"
],
0,
"6a1694a9b4a0c2fb91095dd6c7b7c2da"
],
[
"Spec.HKDF.expand0",
4,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint8",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.bytes",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_1d9166622f9d5c9d61386ed36d354fbf",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Seq.Base.length"
],
0,
"0b20075f1b603b4fe1df4a98a389b4dc"
],
[
"Spec.HKDF.expand",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.W128",
"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_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_FStar.Integers.W128@tok",
"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_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.Integers.width_of_sw", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"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_Spec.Hash.Definitions.hash_alg",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"97935276d75be93f5944958b4339c997"
],
[
"Spec.HKDF.expand",
2,
2,
1,
[
"@query", "constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.W128",
"constructor_distinct_FStar.Integers.Winfinite",
"equality_tok_FStar.Integers.W128@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_FStar.Integers.width_of_sw",
"projection_inverse_FStar.Integers.Signed__0"
],
0,
"14ae305a3a76e1d87867385d1709e274"
],
[
"Spec.HKDF.expand",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_4c22edf297190908ef58dfd960fb9ac5",
"refinement_interpretation_Tm_refine_93a6f01b8db682f6bc12e718db5c8201",
"refinement_interpretation_Tm_refine_ccfcd81f56a06748dbff6bf6b7ba15d8"
],
0,
"6623519199c9dff6c810d7c1634116aa"
]
]
]
Computing file changes ...
