Revision 059787e63538941130606248805cab290fdbc5d7 authored by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC, committed by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC
1 parent 03f1e46
Spec.Agile.HPKE.fst.hints
[
"�$��\\o\u0000�E�H*��",
[
[
"Spec.Agile.HPKE.size_aead_nonce",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"data_elim_FStar.Pervasives.Native.Mktuple3",
"data_typing_intro_Spec.Agile.AEAD.AES256_GCM@tok",
"data_typing_intro_Spec.Agile.DH.DH_P256@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_FStar.Pervasives.inversion", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.Agile.AEAD.iv_length",
"equation_Spec.Agile.HPKE.aead_of_cs",
"equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"fuel_guarded_inversion_Spec.Agile.AEAD.alg", "inversion-interp",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"a897f32e4b579b54ca554bcc7fd3e80f"
],
[
"Spec.Agile.HPKE.size_aead_key",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.AEAD.AES128_GCM",
"constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg",
"equation_Spec.Agile.AEAD.key_length",
"equation_Spec.Agile.HPKE.aead_of_cs",
"equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"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_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.Cipher.key_length",
"typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Spec.Agile.Cipher.AES128@tok",
"typing_tok_Spec.Agile.Cipher.CHACHA20@tok"
],
0,
"5733b5a6b022318d8d99da8bb96cb0fa"
],
[
"Spec.Agile.HPKE.size_aead_tag",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"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.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.tag_length",
"equation_Spec.Agile.HPKE.aead_of_cs",
"equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"fuel_guarded_inversion_Spec.Agile.AEAD.alg",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.Agile.HPKE.aead_of_cs",
"typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"aabf6bcb0dd72834fc0da76016f96237"
],
[
"Spec.Agile.HPKE.size_dh_public",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.DH.DH_P256",
"disc_equation_Spec.Agile.DH.DH_Curve25519",
"disc_equation_Spec.Agile.DH.DH_P256",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.GaloisField.gf",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"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_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.Agile.DH.size_public",
"typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Spec.Agile.DH.DH_P256@tok"
],
0,
"67a15c3e347ab84e8c4379586235cdbe"
],
[
"Spec.Agile.HPKE.size_kdf",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"data_typing_intro_Spec.Agile.AEAD.AES256_GCM@tok",
"data_typing_intro_Spec.Agile.DH.DH_P256@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.hash_of_cs",
"equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.size_hash",
"equation_Spec.Hash.Definitions.word_length",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"int_inversion", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.Agile.HPKE.hash_of_cs",
"typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Hash.Definitions.hash_word_length",
"typing_Spec.Hash.Definitions.word_length",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"879280b524c2f44a02773803c954bf44"
],
[
"Spec.Agile.HPKE.max_length",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"data_typing_intro_Spec.Agile.AEAD.AES256_GCM@tok",
"data_typing_intro_Spec.Agile.DH.DH_P256@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.Integers.int_t",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.Agile.AEAD.max_length",
"equation_Spec.Agile.HPKE.aead_of_cs",
"equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"int_inversion", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"6ebe13c82a0865b87ebe8600df041e0f"
],
[
"Spec.Agile.HPKE.max_pskID",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"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_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"d59ca603001cc910a1123108ef7da8fe"
],
[
"Spec.Agile.HPKE.max_info",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"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_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"63e514b79a8a03297bed69ad2568f25a"
],
[
"Spec.Agile.HPKE.pow2_61",
1,
2,
1,
[ "@query" ],
0,
"d2ef30e7f4d532b264acd5b4244a3490"
],
[
"Spec.Agile.HPKE.pow2_35_less_than_pow2_61",
1,
2,
1,
[ "@query" ],
0,
"9b695acd0ae2dbb885618d98d83ce9f1"
],
[
"Spec.Agile.HPKE.pow2_35_less_than_pow2_125",
1,
2,
1,
[ "@query" ],
0,
"d9215a6d8ee089ea5acc740015d68b5a"
],
[
"Spec.Agile.HPKE.size_label_nonce",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"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_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"9818f6cd789a06d239928207c5a19058"
],
[
"Spec.Agile.HPKE.size_label_key",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"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_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"019e695733ee0708db4677cf323fc121"
],
[
"Spec.Agile.HPKE.label_nonce_list",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.pow2_3", "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_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
"typing_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"9af7d995d9a5f3fe3c50c69415a7d1f4"
],
[
"Spec.Agile.HPKE.label_key_list",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.pow2_3", "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_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
"typing_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"297efa0f07da90eaead855ec6c61e8ce"
],
[
"Spec.Agile.HPKE.label_nonce",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Agile.HPKE.size_label_nonce"
],
0,
"9d373be3dde4521929279e7886a9b5f2"
],
[
"Spec.Agile.HPKE.label_key",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Agile.HPKE.size_label_key"
],
0,
"9a99dfa0cb3311224d823342c3e54e13"
],
[
"Spec.Agile.HPKE.size_cs_identifier",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"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_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"6aaeed939d6f9881ee65289d40d99344"
],
[
"Spec.Agile.HPKE.size_mode_identifier",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"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_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"74c594554b0d85cf4171e1b6d3c274e6"
],
[
"Spec.Agile.HPKE.id_kem",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"da8363aea14a20af31f85b9cb187e7a8"
],
[
"Spec.Agile.HPKE.id_kem",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Spec.Agile.DH.DH_Curve25519",
"disc_equation_Spec.Agile.DH.DH_P256",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.v", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"a69cef1620f86a365dd7472f7d0e322b"
],
[
"Spec.Agile.HPKE.id_kdf",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"66c8b7efa1888baa799468127355343f"
],
[
"Spec.Agile.HPKE.id_kdf",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"data_typing_intro_Spec.Agile.AEAD.AES256_GCM@tok",
"data_typing_intro_Spec.Agile.DH.DH_P256@tok",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.v", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred", "typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"d6fe96dfceffb8352a29627b9198503d"
],
[
"Spec.Agile.HPKE.id_aead",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"d9a6a71297c2660726bdddb5d65e9219"
],
[
"Spec.Agile.HPKE.id_aead",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"data_elim_FStar.Pervasives.Native.Mktuple3",
"data_typing_intro_Spec.Agile.AEAD.AES256_GCM@tok",
"data_typing_intro_Spec.Agile.DH.DH_P256@tok",
"disc_equation_Spec.Agile.AEAD.AES128_GCM",
"disc_equation_Spec.Agile.AEAD.AES256_GCM",
"disc_equation_Spec.Agile.AEAD.CHACHA20_POLY1305",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Prims.squash", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.uu___2",
"equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"fuel_guarded_inversion_Spec.Agile.AEAD.alg",
"function_token_typing_Spec.Agile.AEAD.uu___2", "int_typing",
"inversion-interp", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.v", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred", "typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"bd57cafef42994e8c9732792b53cbe77"
],
[
"Spec.Agile.HPKE.id_of_cs",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"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_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"07f470f4bfb62af192b57768398ee2a4"
],
[
"Spec.Agile.HPKE.id_of_mode",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Spec.Agile.HPKE.Auth",
"disc_equation_Spec.Agile.HPKE.Base",
"disc_equation_Spec.Agile.HPKE.PSK",
"disc_equation_Spec.Agile.HPKE.PSKAuth",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.HPKE.mode", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.v", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"74e620085e5422f2e55def9e024a7b61"
],
[
"Spec.Agile.HPKE.point_compress",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"constructor_distinct_Lib.IntTypes.U8",
"data_typing_intro_Spec.Agile.AEAD.AES256_GCM@tok",
"data_typing_intro_Spec.Agile.DH.DH_P256@tok",
"disc_equation_Spec.Agile.DH.DH_Curve25519",
"disc_equation_Spec.Agile.DH.DH_P256",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.key_dh_public_s",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_inversion",
"primitive_Prims.op_Addition", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"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_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"eecc6fc125d2fbeb12f08071590d4e37"
],
[
"Spec.Agile.HPKE.point_decompress",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.DH.DH_P256",
"data_typing_intro_Spec.Agile.AEAD.AES256_GCM@tok",
"data_typing_intro_Spec.Agile.DH.DH_P256@tok",
"disc_equation_Spec.Agile.DH.DH_Curve25519",
"disc_equation_Spec.Agile.DH.DH_P256",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.DH.serialized_point",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.v", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred", "typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"7e5bf9569c66a71a183cf2f81897d629"
],
[
"Spec.Agile.HPKE.decap",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Spec.Agile.DH.dh", "equation_Spec.Agile.DH.scalar",
"equation_Spec.Agile.DH.serialized_point",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.key_dh_secret_s",
"equation_Spec.Agile.HPKE.size_dh_key",
"lemma_FStar.Pervasives.invertOption", "typing_Spec.Agile.DH.dh",
"typing_Spec.Agile.DH.serialized_point",
"typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.point_compress"
],
0,
"e9eda94eb9bc17cf279b6bdafab9a9f6"
],
[
"Spec.Agile.HPKE.auth_encap",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Agile.DH.DH_P256",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.DH.size_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"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_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"97db95795f94b24f72ae3dd214678d33"
],
[
"Spec.Agile.HPKE.auth_encap",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Agile.DH.DH_P256",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.DH.size_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"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_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"689fd122126d00bba0ca8c75ff3329cf"
],
[
"Spec.Agile.HPKE.auth_decap",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Agile.DH.DH_P256",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.DH.size_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"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_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"1acd5a81cca5c03a080167623ec6ffa2"
],
[
"Spec.Agile.HPKE.auth_decap",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Agile.DH.DH_P256",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.DH.size_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"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_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"99f2fddb541c149db6beec4f049a5a67"
],
[
"Spec.Agile.HPKE.default_pkI",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.v", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"5776c46ab6631130025d08cfc6a06bf3"
],
[
"Spec.Agile.HPKE.default_psk",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.v", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"9954cb4c8e7d21afeef2b2149bdf3bf9"
],
[
"Spec.Agile.HPKE.default_pskId",
1,
1,
1,
[ "@query" ],
0,
"1b4787db0f4037c90ad14966e8ba6e33"
],
[
"Spec.Agile.HPKE.build_context",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"6f544ca54b402382fcfee749153cc001"
],
[
"Spec.Agile.HPKE.build_context",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"34b522d21986954ad9f9a19699e94d8c"
],
[
"Spec.Agile.HPKE.build_context",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"data_typing_intro_Spec.Agile.AEAD.AES256_GCM@tok",
"data_typing_intro_Spec.Agile.DH.DH_P256@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.hash_of_cs",
"equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.Agile.HPKE.size_cs_identifier",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.Agile.HPKE.size_mode_identifier",
"equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.size_hash",
"equation_Spec.Hash.Definitions.word_length",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_3",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"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_1e70925eac6491cc483a551daf513891",
"refinement_interpretation_Tm_refine_3c588f78111fe6f21efdce83398090c4",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_eadc61dc42940bbe5de43f757eae7508",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Prims.pow2", "typing_Spec.AES.gf8",
"typing_Spec.Agile.DH.size_public",
"typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.hash_of_cs",
"typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok",
"typing_tok_Spec.Agile.DH.DH_Curve25519@tok"
],
0,
"3322300cd2650b33b245e5f3581a2ca1"
],
[
"Spec.Agile.HPKE.ks_derive",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"6ef17cf7a3df8a9b4c296886564ad6bd"
],
[
"Spec.Agile.HPKE.ks_derive",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"93768a5dd33ee1578fb1654538983bb9"
],
[
"Spec.Agile.HPKE.ks_derive",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.AES.AES128",
"constructor_distinct_Spec.Agile.AEAD.AES128_GCM",
"constructor_distinct_Spec.Agile.Cipher.AES128",
"constructor_distinct_Spec.Agile.Cipher.CHACHA20",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"data_elim_FStar.Pervasives.Native.Mktuple3",
"data_typing_intro_Spec.Agile.AEAD.AES256_GCM@tok",
"data_typing_intro_Spec.Agile.DH.DH_P256@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.AES.AES128@tok",
"equality_tok_Spec.Agile.Cipher.AES128@tok",
"equality_tok_Spec.Agile.Cipher.CHACHA20@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Prims.squash", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.AES.key_size",
"equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg",
"equation_Spec.Agile.AEAD.key_length",
"equation_Spec.Agile.AEAD.uu___2",
"equation_Spec.Agile.Cipher.aes_alg_of_alg",
"equation_Spec.Agile.Cipher.key_length",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HKDF.lbytes",
"equation_Spec.Agile.HMAC.keysized",
"equation_Spec.Agile.HPKE.aead_of_cs",
"equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.default_pkI",
"equation_Spec.Agile.HPKE.default_psk",
"equation_Spec.Agile.HPKE.default_pskId",
"equation_Spec.Agile.HPKE.hash_of_cs",
"equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.Agile.HPKE.key_dh_public_s",
"equation_Spec.Agile.HPKE.label_key",
"equation_Spec.Agile.HPKE.label_nonce",
"equation_Spec.Agile.HPKE.max_info",
"equation_Spec.Agile.HPKE.max_pskID",
"equation_Spec.Agile.HPKE.pow2_35_less_than_pow2_125",
"equation_Spec.Agile.HPKE.pow2_35_less_than_pow2_61",
"equation_Spec.Agile.HPKE.pow2_61", "equation_Spec.Agile.HPKE.psk_s",
"equation_Spec.Agile.HPKE.size_aead_key",
"equation_Spec.Agile.HPKE.size_aead_nonce",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.Agile.HPKE.size_kdf",
"equation_Spec.Agile.HPKE.size_label_key",
"equation_Spec.Agile.HPKE.size_label_nonce",
"equation_Spec.Agile.HPKE.size_psk",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.max_input_length",
"equation_Spec.Hash.Definitions.size_hash",
"equation_Spec.Hash.Definitions.word_length",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"fuel_guarded_inversion_Spec.Agile.AEAD.alg",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Spec.Agile.AEAD.uu___2",
"function_token_typing_Spec.Agile.HPKE.pow2_35_less_than_pow2_125",
"function_token_typing_Spec.Agile.HPKE.pow2_35_less_than_pow2_61",
"function_token_typing_Spec.Agile.HPKE.pow2_61", "int_inversion",
"int_typing", "inversion-interp",
"kinding_FStar.Pervasives.Native.tuple2@tok",
"lemma_FStar.Pervasives.invertOption",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_3",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.None_a",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0a4f93cd9b0922c70a50cc32652be606",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_29c27ac7c716b2238749315b70c9eca3",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_3c6f335880cd1199c873ba053c707b1b",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_4d6c12d91ad48195cce7aa69db5924e9",
"refinement_interpretation_Tm_refine_4ebfd0e83376a15979ce8403ef0ca858",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_83df305ec3ddfee7d9a46b4fea237569",
"refinement_interpretation_Tm_refine_889261280ac78161e61fb5281df9a8c1",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_b1ad91029171789e0c66dd561092f84e",
"refinement_interpretation_Tm_refine_d820be43ac1c36de7a505d4da0fc7967",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e2b45c7bb19eecebc754851bbc30c994",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"refinement_kinding_Tm_refine_4ebfd0e83376a15979ce8403ef0ca858",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.v", "typing_Lib.Sequence.create",
"typing_Spec.AES.gf8", "typing_Spec.AES.irred",
"typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.default_pskId",
"typing_Spec.Agile.HPKE.hash_of_cs",
"typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.Agile.HPKE.label_key",
"typing_Spec.Agile.HPKE.label_nonce",
"typing_Spec.Agile.HPKE.max_info", "typing_Spec.Agile.HPKE.psk_s",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.Agile.HPKE.size_psk",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Hash.Definitions.max_input_length",
"typing_Spec.Hash.Definitions.size_hash",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"c902cca6d0fa19f735a7506272916b57"
],
[
"Spec.Agile.HPKE.setupBaseI",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "data_elim_Spec.GaloisField.GF",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8"
],
0,
"958e093873f527c53c923c35e11435b1"
],
[
"Spec.Agile.HPKE.setupBaseI",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "data_elim_Spec.GaloisField.GF",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8"
],
0,
"db196d26362f7efb229401ee764f13aa"
],
[
"Spec.Agile.HPKE.setupBaseI",
3,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "bool_typing",
"data_typing_intro_Spec.Agile.AEAD.AES256_GCM@tok",
"data_typing_intro_Spec.Agile.DH.DH_P256@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.encap",
"equation_Spec.Agile.HPKE.key_dh_public_s",
"equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"kinding_FStar.Pervasives.Native.tuple2@tok",
"lemma_FStar.Pervasives.invertOption",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.encap",
"typing_Spec.Agile.HPKE.key_dh_public_s",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"7e4efe727027bb481266d9ebac1573fc"
],
[
"Spec.Agile.HPKE.setupBaseR",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "data_elim_Spec.GaloisField.GF",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8"
],
0,
"107b8ec502fa645ad0aa8896fe382e1c"
],
[
"Spec.Agile.HPKE.setupBaseR",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "data_elim_Spec.GaloisField.GF",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8"
],
0,
"efa616be80cc7560390d4bd19fc426b5"
],
[
"Spec.Agile.HPKE.setupBaseR",
3,
1,
1,
[
"@MaxIFuel_assumption", "@query", "data_elim_Spec.GaloisField.GF",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8"
],
0,
"af279844db8b65bf1f8c53fea5621b8c"
],
[
"Spec.Agile.HPKE.setupAuthI",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "data_elim_Spec.GaloisField.GF",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8"
],
0,
"431ce707aa045499b1ae1b37d2658a3b"
],
[
"Spec.Agile.HPKE.setupAuthI",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "data_elim_Spec.GaloisField.GF",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8"
],
0,
"a9d06b6f288d76675e7bb7e36690b1ba"
],
[
"Spec.Agile.HPKE.setupAuthI",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Agile.DH.DH_P256",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.max_info",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"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_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.max_info",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"428d1c2b249ec7a839688974492b2263"
],
[
"Spec.Agile.HPKE.setupAuthR",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "data_elim_Spec.GaloisField.GF",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8"
],
0,
"320f5cd982212acc3c626563bdb36234"
],
[
"Spec.Agile.HPKE.setupAuthR",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "data_elim_Spec.GaloisField.GF",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8"
],
0,
"d539b16fdbe5423306c4f0355f63b0a6"
],
[
"Spec.Agile.HPKE.setupAuthR",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Agile.DH.DH_P256",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.max_info",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"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_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.max_info",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"4d0ec26334d898712494766b282134b5"
],
[
"Spec.Agile.HPKE.setupAuthPSKI",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"b3577b71841b6bfabe56449aabad7dbf"
],
[
"Spec.Agile.HPKE.setupAuthPSKI",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"8b90e310da0dd7b4cd711e45d7017ed8"
],
[
"Spec.Agile.HPKE.setupAuthPSKI",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Agile.DH.DH_P256",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.max_pskID",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"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_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.max_pskID",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"c0e0da00a37d28d979acd93236c699b8"
],
[
"Spec.Agile.HPKE.setupPSKAuthR",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"0589399fbd0655041ef46d629626f716"
],
[
"Spec.Agile.HPKE.setupPSKAuthR",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"175505290f8be66ade233f40d9c1fe7b"
],
[
"Spec.Agile.HPKE.setupPSKAuthR",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Agile.DH.DH_Curve25519",
"constructor_distinct_Spec.Agile.DH.DH_P256",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.max_info",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"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_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.max_info",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"f2465ea2a22253281c23268d962ca47e"
],
[
"Spec.Agile.HPKE.sealBase",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"1483f139a3adfc058087af84b40845fb"
],
[
"Spec.Agile.HPKE.sealBase",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"6e0719272f1cc6781dd614f3b0f05177"
],
[
"Spec.Agile.HPKE.sealBase",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"data_typing_intro_Spec.Agile.AEAD.AES256_GCM@tok",
"data_typing_intro_Spec.Agile.DH.DH_P256@tok",
"disc_equation_FStar.Pervasives.Native.None",
"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_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.Agile.AEAD.iv_length",
"equation_Spec.Agile.AEAD.max_length",
"equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.DH.size_key",
"equation_Spec.Agile.HPKE.aead_of_cs",
"equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.is_ciphersuite",
"equation_Spec.Agile.HPKE.key_aead_s",
"equation_Spec.Agile.HPKE.key_dh_public_s",
"equation_Spec.Agile.HPKE.max_info",
"equation_Spec.Agile.HPKE.max_length",
"equation_Spec.Agile.HPKE.nonce_aead_s",
"equation_Spec.Agile.HPKE.size_aead_key",
"equation_Spec.Agile.HPKE.size_aead_nonce",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"int_inversion", "int_typing",
"kinding_FStar.Pervasives.Native.tuple3@tok",
"lemma_FStar.Pervasives.invertOption",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_4",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0cc80117eb21421f0d463f0a6faa28e1",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_3c6f335880cd1199c873ba053c707b1b",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a1975f512ae8d6b6a4d92fbdf441bb00",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.Agile.HPKE.key_aead_s",
"typing_Spec.Agile.HPKE.key_dh_public_s",
"typing_Spec.Agile.HPKE.max_info",
"typing_Spec.Agile.HPKE.nonce_aead_s",
"typing_Spec.Agile.HPKE.setupBaseI",
"typing_Spec.Agile.HPKE.size_aead_nonce",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"1cb859d296973c0daa415b44b6ca39eb"
],
[
"Spec.Agile.HPKE.openBase",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"a37b2cb9a195e4a2ca7e2274fbff47b5"
],
[
"Spec.Agile.HPKE.openBase",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"2cd58d14e568bc9c17749fb8ded50e85"
],
[
"Spec.Agile.HPKE.openBase",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.AEAD_pretyping_41331a91ff12fcf941445c36290a4fc0",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "bool_typing",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"data_typing_intro_Spec.Agile.AEAD.AES256_GCM@tok",
"data_typing_intro_Spec.Agile.DH.DH_P256@tok",
"disc_equation_FStar.Pervasives.Native.None",
"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_FStar.Integers.Winfinite@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equality_tok_Spec.Agile.DH.DH_Curve25519@tok",
"equality_tok_Spec.Agile.DH.DH_P256@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.Agile.AEAD.iv_length",
"equation_Spec.Agile.AEAD.max_length",
"equation_Spec.Agile.AEAD.tag_length",
"equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.DH.size_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.aead_of_cs",
"equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.curve_of_cs",
"equation_Spec.Agile.HPKE.key_aead_s",
"equation_Spec.Agile.HPKE.key_dh_public_s",
"equation_Spec.Agile.HPKE.max_info",
"equation_Spec.Agile.HPKE.nonce_aead_s",
"equation_Spec.Agile.HPKE.setupBaseR",
"equation_Spec.Agile.HPKE.size_aead_key",
"equation_Spec.Agile.HPKE.size_aead_nonce",
"equation_Spec.Agile.HPKE.size_aead_tag",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Curve25519.one",
"equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"fuel_guarded_inversion_Spec.Agile.AEAD.alg",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "kinding_FStar.Pervasives.Native.tuple2@tok",
"lemma_FStar.Pervasives.invertOption",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0cc80117eb21421f0d463f0a6faa28e1",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_3c6f335880cd1199c873ba053c707b1b",
"refinement_interpretation_Tm_refine_4b7104deadfa7fc29e5a120f5b0ea436",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7087bb9f7385184591d10c61617cb0c4",
"refinement_interpretation_Tm_refine_7eec435bed21a0f9089c1978e6ee3b8d",
"refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955",
"refinement_interpretation_Tm_refine_9b8b991835088c05805a568c0485d476",
"refinement_interpretation_Tm_refine_ba2b797d3e0211cc8daf210df7ba8624",
"refinement_interpretation_Tm_refine_d2be20cb22a400c3971df31bf7513225",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.Agile.AEAD.tag_length",
"typing_Spec.Agile.HPKE.aead_of_cs",
"typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.key_aead_s",
"typing_Spec.Agile.HPKE.max_info",
"typing_Spec.Agile.HPKE.nonce_aead_s",
"typing_Spec.Agile.HPKE.setupBaseR",
"typing_Spec.Agile.HPKE.size_aead_nonce",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"d88b9c9e3b9f1ff413beaaecc68d6556"
]
]
]
Computing file changes ...
