Revision 724d1045f60f13d79df1afc5190955afdfa73ec1 authored by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC, committed by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC
Co-authored-by: @protz
1 parent ca37fbf
Hacl.HPKE.Curve51_CP256_SHA512.fsti.hints
[
"��Ә���X\u000f��\u0013�'H",
[
[
"Hacl.HPKE.Curve51_CP256_SHA512.setupBaseI",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"c86dab582fadcb1784a715336c685b4e"
],
[
"Hacl.HPKE.Curve51_CP256_SHA512.setupBaseR",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"6f414394f96e8f2d07e6cff5801ec406"
],
[
"Hacl.HPKE.Curve51_CP256_SHA512.sealBase",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"f1cd4fd9b5220f2d70898ed28cac6149"
],
[
"Hacl.HPKE.Curve51_CP256_SHA512.openBase",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"08304e154b50ec38608b1cbfa2148606"
]
]
]
Computing file changes ...
