[ "ݶ*\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, "d7fc6002a6024332ef1b2ac645545819" ], [ "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, "e836de27c463c2856deba08a1800060c" ], [ "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, "837d661d2111858fd2cdd8b228f00cf5" ], [ "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, "2449363aafc40d381806fc8595a22f08" ] ] ]