Revision aa1ca8698adfe929a9eff86ac143eaf90fc3e8ee authored by Jay Bosamiya on 03 June 2019, 21:51:38 UTC, committed by Jay Bosamiya on 03 June 2019, 21:51:38 UTC
1 parent 6055e85
Hacl.HMAC.fsti.hints
[
"�ob�tP\r \u0002��]�Liq",
[
[
"Hacl.HMAC.key_and_data_fits",
1,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.W128",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W128@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_FStar.Integers.width_of_sw", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.max_input_length",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"5d24108346fd013ba78dde5dfd5e16aa"
],
[
"Hacl.HMAC.compute_st",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.Winfinite@tok",
"equation_EverCrypt.Helpers.uint8_p",
"equation_EverCrypt.Helpers.uint8_t",
"equation_FStar.Integers.int_t", "equation_LowStar.Buffer.buffer",
"equation_Prims.nat", "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_FStar.UInt8.t", "int_inversion",
"lemma_LowStar.Monotonic.Buffer.length_as_seq",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"refinement_interpretation_Tm_refine_0879c107c66fba8772fecae610c19578",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d31cd115930e46a8b73a31bb5e929899",
"typing_LowStar.Buffer.trivial_preorder",
"typing_Spec.Hash.Definitions.max_input_length",
"typing_Spec.Hash.Definitions.word_length"
],
0,
"af81de02e6ad05b96d038cfdc9180039"
]
]
]
Computing file changes ...