Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
Hacl.Impl.HPKE.fsti.hints
[
"ݶ�����*\u001el�ҍ\nZ",
[
[
"Hacl.Impl.HPKE.setupBaseI_st",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Impl.HPKE.key_aead",
"equation_Hacl.Impl.HPKE.key_dh_public",
"equation_Hacl.Impl.HPKE.nonce_aead", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.HPKE.size_aead_nonce",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem", "lemma_Lib.IntTypes.v_mk_int",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9290139726e186fc22145f97d07b3d7e",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.Buffer.length", "typing_Spec.AES.gf8",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"2355ce8f3deb3e7b94d892ff219fb9a3"
],
[
"Hacl.Impl.HPKE.setupBaseR_st",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Impl.HPKE.key_aead",
"equation_Hacl.Impl.HPKE.key_dh_secret",
"equation_Hacl.Impl.HPKE.nonce_aead", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Agile.HPKE.size_aead_nonce",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Spec.AES.elem", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.IntTypes.v_mk_int", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9290139726e186fc22145f97d07b3d7e",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"c2dbbeb59020ee7fcb3ec3671dfc73b7"
],
[
"Hacl.Impl.HPKE.sealBase_st",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.AEAD.AES128_GCM@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.lseq", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"function_token_typing_Spec.AES.elem", "lemma_Lib.IntTypes.v_mk_int",
"primitive_Prims.op_Addition", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9290139726e186fc22145f97d07b3d7e",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_baf813066c2e5ec93c62e1ddaebe698f",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.Buffer.length", "typing_Lib.IntTypes.v",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Agile.AEAD.AES128_GCM@tok",
"typing_tok_Spec.Agile.DH.DH_Curve25519@tok"
],
0,
"f773b91d9d0b3d392f6a407a3c3bf6e7"
],
[
"Hacl.Impl.HPKE.openBase_st",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.AEAD.AES128_GCM@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.max_length",
"equation_Spec.Agile.HPKE.size_aead_tag",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_70657450067a0998493a3a2680432026",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955",
"refinement_interpretation_Tm_refine_9290139726e186fc22145f97d07b3d7e",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.tag_length",
"typing_Spec.Agile.HPKE.aead_of_cs",
"typing_Spec.Agile.HPKE.max_length",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Agile.AEAD.AES128_GCM@tok",
"typing_tok_Spec.Agile.DH.DH_Curve25519@tok"
],
0,
"d604f47812936728c1214d38421f514a"
]
]
]
Computing file changes ...
