[ "l/d\u0016$=\u0018B", [ [ "Hacl.HPKE.P256_CP128_SHA256.setupBaseI", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.DH.DH_P256", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "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_P256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@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.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, "f8c11b2e2226d68c921920285b2cb229" ], [ "Hacl.HPKE.P256_CP128_SHA256.setupBaseI", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0", "Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.DH.DH_P256", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "disc_equation_FStar.Pervasives.Native.Some", "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", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.DH.DH_Curve25519@tok", "equality_tok_Spec.Agile.DH.DH_P256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.curve_of_cs", "equation_Spec.Agile.HPKE.hash_of_cs", "equation_Spec.Agile.HPKE.is_ciphersuite", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "function_token_typing_Spec.AES.elem", "lemma_FStar.UInt32.uv_inv", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "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_0337823f2b140592b868d0aa48aba59e", "refinement_interpretation_Tm_refine_328939acd293d2a3ec5363f0b37707b5", "refinement_interpretation_Tm_refine_7dee8852a19715c9524d9f964bc908ae", "refinement_interpretation_Tm_refine_90288dc698ceec6eec0fe95cef5c7196", "refinement_interpretation_Tm_refine_a5d095a095dea057a7045c397f91782f", "refinement_interpretation_Tm_refine_bf80a6c184f17b23752b55d0dd5d8321", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Spec.Agile.AEAD.AES128_GCM@tok", "typing_tok_Spec.Agile.DH.DH_Curve25519@tok" ], 0, "a5db513e9c5ae0b787f995a2a3ee3569" ], [ "Hacl.HPKE.P256_CP128_SHA256.setupBaseR", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.DH.DH_P256", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "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_P256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@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.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, "e05a8774d485be6c7c12c413d88efb06" ], [ "Hacl.HPKE.P256_CP128_SHA256.setupBaseR", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0", "Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.DH.DH_P256", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "disc_equation_FStar.Pervasives.Native.Some", "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", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.DH.DH_Curve25519@tok", "equality_tok_Spec.Agile.DH.DH_P256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.curve_of_cs", "equation_Spec.Agile.HPKE.hash_of_cs", "equation_Spec.Agile.HPKE.is_ciphersuite", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "function_token_typing_Spec.AES.elem", "lemma_FStar.UInt32.uv_inv", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Integers.Signed__0", "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_0337823f2b140592b868d0aa48aba59e", "refinement_interpretation_Tm_refine_328939acd293d2a3ec5363f0b37707b5", "refinement_interpretation_Tm_refine_7dee8852a19715c9524d9f964bc908ae", "refinement_interpretation_Tm_refine_90288dc698ceec6eec0fe95cef5c7196", "refinement_interpretation_Tm_refine_a5d095a095dea057a7045c397f91782f", "refinement_interpretation_Tm_refine_bf80a6c184f17b23752b55d0dd5d8321", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Spec.Agile.AEAD.AES128_GCM@tok", "typing_tok_Spec.Agile.DH.DH_Curve25519@tok" ], 0, "7401ac7fab7102b4ddf4eff33e3ddd21" ], [ "Hacl.HPKE.P256_CP128_SHA256.sealBase", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.DH.DH_P256", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "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_P256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@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.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, "faa2e88732aee38723293959fbb6a31c" ], [ "Hacl.HPKE.P256_CP128_SHA256.sealBase", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0", "Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.DH.DH_P256", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.DH.DH_Curve25519@tok", "equality_tok_Spec.Agile.DH.DH_P256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.aead_of_cs", "equation_Spec.Agile.HPKE.is_ciphersuite", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "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", "typing_tok_Spec.Agile.AEAD.AES128_GCM@tok", "typing_tok_Spec.Agile.DH.DH_Curve25519@tok" ], 0, "2c18a888713ff6927d5336f088a47034" ], [ "Hacl.HPKE.P256_CP128_SHA256.openBase", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.DH.DH_P256", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "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_P256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@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.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, "561f2b54eee0e3d4110447a1bd4f3f1a" ], [ "Hacl.HPKE.P256_CP128_SHA256.openBase", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0", "Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305", "constructor_distinct_Spec.Agile.DH.DH_P256", "constructor_distinct_Spec.Hash.Definitions.SHA2_256", "disc_equation_FStar.Pervasives.Native.Some", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.DH.DH_Curve25519@tok", "equality_tok_Spec.Agile.DH.DH_P256@tok", "equality_tok_Spec.Hash.Definitions.SHA2_256@tok", "equation_Lib.Buffer.as_seq", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.aead_of_cs", "equation_Spec.Agile.HPKE.is_ciphersuite", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_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", "typing_tok_Spec.Agile.AEAD.AES128_GCM@tok", "typing_tok_Spec.Agile.DH.DH_Curve25519@tok" ], 0, "e9ebc0d2ebe43a1e32b8f504ff88ad9b" ] ] ]