https://github.com/project-everest/hacl-star
Tip revision: 4d41d4ec3acc48721e2966ccf1a9a9abdaadc719 authored by Chris Hawblitzel on 14 March 2019, 05:53:02 UTC
Disable X64.Leakage_Ins* to enable merge
Disable X64.Leakage_Ins* to enable merge
Tip revision: 4d41d4e
Hacl.Impl.Chacha20Poly1305.fsti.hints
[
"!.eL`܊���\f�\u001d�\tG",
[
[
"Hacl.Impl.Chacha20Poly1305.aead_encrypt_chacha_poly",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Spec.Chacha20.blocklen",
"equation_Spec.Chacha20Poly1305.size_block",
"equation_Spec.Poly1305.size_block",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_7af8c0c820f0fddc486a546dd953faa1",
"refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
"typing_Lib.IntTypes.uint_v", "typing_tok_Lib.Buffer.MUT@tok",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"81b5df32f3dba3ef97361bdda37b4ae5"
],
[
"Hacl.Impl.Chacha20Poly1305.aead_decrypt_chacha_poly",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.Buffer.as_seq",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.uint_v",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Spec.Chacha20Poly1305.size_block",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"function_token_typing_Lib.IntTypes.uint8",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_7af8c0c820f0fddc486a546dd953faa1",
"refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.Buffer.as_seq", "typing_Lib.IntTypes.uint_v",
"typing_Spec.Poly1305.size_key", "typing_tok_Lib.Buffer.MUT@tok",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"71bf2b2cf13a8bd4f0c16f505effa814"
]
]
]