Revision 1068d4afc039dbd12db6dbce298cdb0962d6d224 authored by Aymeric Fromherz on 01 April 2019, 04:39:20 UTC, committed by Aymeric Fromherz on 01 April 2019, 04:39:20 UTC
1 parent d7fe03c
EverCrypt.HKDF.fsti.hints
[
"\u0013���;�\u0012I(\u0011[$o\rK+",
[
[
"EverCrypt.HKDF.expand0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_FStar.Integers.int_t", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word_length",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"7518a5e04106fc27c6429afb2cd5d703"
],
[
"EverCrypt.HKDF.expand0",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"binder_x_332103d8b337802efb5758d608edf05f_0",
"binder_x_6b79df958d1653847f8ecfa6e77b3dfc_5",
"binder_x_8bd955e02b68cbc36564bcb80ea85ae4_2",
"binder_x_8f6b7d31a6c4f79fd56967adbaedd2d5_3",
"binder_x_8f6b7d31a6c4f79fd56967adbaedd2d5_4", "bool_inversion",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.HMAC.lbytes", "equation_FStar.Integers.int",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.nat",
"equation_FStar.Integers.uint_8",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Seq.Base.op_At_Bar",
"equation_FStar.Seq.Properties.split", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Prims.nat",
"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.state_word_length",
"equation_Spec.Hash.Definitions.word_length",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"function_token_typing_FStar.Integers.uint_8",
"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_AmpAmp", "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_8a88f84ddb86f6a45826b1d92939a27c",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_dd6fa80cd78a4a401dbf2731186ee3f8",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
"typing_FStar.UInt.max_int", "well-founded-ordering-on-nat"
],
0,
"8ef9134b83f798798e27400171576f2e"
],
[
"EverCrypt.HKDF.expand0",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W8",
"equality_tok_FStar.Integers.W8@tok",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.bytes",
"function_token_typing_FStar.Integers.uint_8",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_3ac913f42eadbb09e45b8ab2293e4706",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length"
],
0,
"049906b1721e1296a0d38715d77dc297"
],
[
"EverCrypt.HKDF.expand0",
4,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W8",
"equality_tok_FStar.Integers.W8@tok",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.bytes",
"function_token_typing_FStar.Integers.uint_8",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_3ac913f42eadbb09e45b8ab2293e4706",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length"
],
0,
"ec3c301638da3d7018b6f83656fd9c80"
],
[
"EverCrypt.HKDF.expand",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Integers.nat",
"refinement_interpretation_Tm_refine_561b19b989af62ac06ac97d973d1c77c"
],
0,
"e486b1c1351eccccb8106c061a73a90f"
],
[
"EverCrypt.HKDF.expand",
2,
2,
1,
[ "@query" ],
0,
"52700fbf307d0d0a36a05ff4333dac4c"
],
[
"EverCrypt.HKDF.hkdf_extract",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"constructor_distinct_Spec.Hash.Definitions.SHA1",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
"equation_LowStar.Buffer.buffer", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.state_word_length",
"equation_Spec.Hash.Definitions.word_length",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"function_token_typing_FStar.Integers.uint_8",
"function_token_typing_FStar.UInt8.t",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_135e9a83a5388912e3ae91df256d2fc7",
"refinement_interpretation_Tm_refine_9b096578fdaf89e78af45d2ef7c6dc07",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_LowStar.Buffer.trivial_preorder",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"bfb8fd5906b462b368f76f21d740eb76"
],
[
"EverCrypt.HKDF.hkdf_expand",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.Seq.Base.seq__uu___haseq",
"assumption_FStar.UInt8.t__uu___haseq", "b2t_def",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Unsigned",
"constructor_distinct_FStar.Integers.W128",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Spec.Hash.Definitions.MD5",
"equality_tok_FStar.Integers.W128@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.Helpers.uint8_l",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.Integers.int_t", "equation_FStar.Integers.uint_8",
"equation_FStar.Integers.v", "equation_FStar.Integers.width_of_sw",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_LowStar.Buffer.buffer",
"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.word_length",
"function_token_typing_FStar.Integers.uint_8",
"function_token_typing_FStar.UInt8.t",
"function_token_typing_Prims.__cache_version_number__",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"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_156677950ba130498d26fd9f8eb20439",
"refinement_interpretation_Tm_refine_b58d02024ba0a69b68a3c96c403806d9",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_LowStar.Buffer.trivial_preorder",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"421ca50b81dcb50864d731d4e4cd7119"
]
]
]
Computing file changes ...
