Revision 8a7e1b7f7f7dda7d9ac75c7adbb915b5c7db208f authored by Dzomo the everest Yak on 09 January 2020, 09:25:31 UTC, committed by Dzomo the everest Yak on 09 January 2020, 09:25:31 UTC
1 parent 9cd0bde
Spec.Agile.HPKE.fst.hints
[
"9�-�D��D�4�[\u0000���",
[
[
"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.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.S16",
"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",
"data_elim_FStar.Pervasives.Native.Mktuple3",
"data_typing_intro_Spec.Agile.DH.DH_Curve448@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@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.algorithm",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_99d574bfd1d8eaa5fe4d7c6d446fa884",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.Agile.AEAD.is_supported_alg",
"typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"538af3f609f44da92940005b2c8e3742"
],
[
"Spec.Agile.HPKE.size_aead_key",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"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.Agile.AEAD.AES128_GCM",
"constructor_distinct_Spec.Agile.AEAD.AES256_GCM",
"constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@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.algorithm",
"equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg",
"equation_Spec.Agile.AEAD.key_length",
"equation_Spec.Agile.AEAD.size_key",
"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",
"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_99d574bfd1d8eaa5fe4d7c6d446fa884",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.Cipher.key_length",
"typing_Spec.Agile.HPKE.aead_of_cs",
"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.AES256@tok",
"typing_tok_Spec.Agile.Cipher.CHACHA20@tok"
],
0,
"4c1a91d9f433f991716c71b187ec1d77"
],
[
"Spec.Agile.HPKE.size_aead_tag",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@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.algorithm",
"equation_Spec.Agile.AEAD.size_tag",
"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", "int_typing",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_99d574bfd1d8eaa5fe4d7c6d446fa884",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.aead_of_cs",
"typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"78468c1270f318732d6e639b0f967898"
],
[
"Spec.Agile.HPKE.size_kdf",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"data_typing_intro_Spec.Agile.DH.DH_Curve448@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@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.algorithm",
"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_typing", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_99d574bfd1d8eaa5fe4d7c6d446fa884",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.hash_of_cs",
"typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"3972871ad0bf0a973e4e57ac0e6599a5"
],
[
"Spec.Agile.HPKE.max_length",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.Signed",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"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.U64",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"data_elim_FStar.Pervasives.Native.Mktuple3",
"data_typing_intro_Spec.Agile.DH.DH_Curve448@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@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.Integers.int_t",
"equation_FStar.Pervasives.inversion", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.algorithm",
"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",
"fuel_guarded_inversion_Spec.Agile.AEAD.alg", "int_inversion",
"inversion-interp", "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_90a1661541e4f009452ab107b47b5955",
"refinement_interpretation_Tm_refine_99d574bfd1d8eaa5fe4d7c6d446fa884",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.Agile.HPKE.is_ciphersuite",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"26bf34f5ca3b6843b9740addade62863"
],
[
"Spec.Agile.HPKE.max_pskID",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"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.W31@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@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",
"lemma_Lib.IntTypes.pow2_4", "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",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Prims.pow2", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"fc7f092b0774bf5cc315211c234ed61b"
],
[
"Spec.Agile.HPKE.max_info",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"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.W31@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@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",
"lemma_Lib.IntTypes.pow2_4", "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",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Prims.pow2", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"52bcbe2513bd001ffc906e1c29b44768"
],
[
"Spec.Agile.HPKE.pow2_61",
1,
2,
1,
[ "@query" ],
0,
"4dad8fcee6d71279caae08ab1b831239"
],
[
"Spec.Agile.HPKE.pow2_35_less_than_pow2_61",
1,
2,
1,
[ "@query" ],
0,
"8d2db1183ad4473a75582d5c7cd86ce8"
],
[
"Spec.Agile.HPKE.pow2_35_less_than_pow2_125",
1,
2,
1,
[ "@query" ],
0,
"52f975cc8d0adea487e6344c6a6a7b6e"
],
[
"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.W31",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"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.W31@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@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,
"84ccd548554f584c2adca13553a6ceaf"
],
[
"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.W31",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"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.W31@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@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,
"b8549f31d14aac203329b60e8a8d533f"
],
[
"Spec.Agile.HPKE.label_nonce_list",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"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",
"equation_Spec.Poly1305.size_key", "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_0ec011aea9f93256a3547ad9f0c667f1",
"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.v", "typing_Prims.pow2", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"79a5f84704b0afaa15995aff0070abd6"
],
[
"Spec.Agile.HPKE.label_key_list",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"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",
"equation_Spec.Poly1305.size_key", "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_0ec011aea9f93256a3547ad9f0c667f1",
"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.v", "typing_Prims.pow2", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_key", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"547e6783dec8087a23dc255c830e2e45"
],
[
"Spec.Agile.HPKE.label_nonce",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Agile.HPKE.size_label_nonce"
],
0,
"090a00d79f28fb1a66f7ddaa281d1a06"
],
[
"Spec.Agile.HPKE.label_key",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"typing_Spec.Agile.HPKE.size_label_key"
],
0,
"92b2ea7e5c48f4598e82746c572cf69e"
],
[
"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.W31",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"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.W31@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@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,
"3f08e4ce1a28e8755d10b86ba6761b79"
],
[
"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.W31",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"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.W31@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@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,
"905c3d8cf3b0c9dc77e3a06bf678567e"
],
[
"Spec.Agile.HPKE.id_of_cs",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"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.Agile.DH.DH_Curve448",
"data_elim_FStar.Pervasives.Native.Mktuple3",
"data_typing_intro_Spec.Agile.DH.DH_Curve448@tok",
"disc_equation_Spec.Agile.AEAD.AES128_GCM",
"disc_equation_Spec.Agile.AEAD.AES256_GCM",
"disc_equation_Spec.Agile.AEAD.CHACHA20_POLY1305",
"disc_equation_Spec.Agile.DH.DH_Curve25519",
"disc_equation_Spec.Agile.DH.DH_Curve448",
"disc_equation_Spec.Agile.DH.DH_P256",
"disc_equation_Spec.Hash.Definitions.SHA2_256",
"disc_equation_Spec.Hash.Definitions.SHA2_512",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_FStar.Pervasives.inversion",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.algorithm",
"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",
"proj_equation_FStar.Pervasives.Native.Mktuple3__1",
"proj_equation_FStar.Pervasives.Native.Mktuple3__2",
"proj_equation_FStar.Pervasives.Native.Mktuple3__3",
"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_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_99d574bfd1d8eaa5fe4d7c6d446fa884",
"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,
"27e6a6b1d0c99f3f4d2be7169051fd47"
],
[
"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.W31",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"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.W31@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@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,
"d4783fa6ab7dc47bfae8fc3d03ecdcb1"
],
[
"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.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@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.DH.size_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf", "int_inversion",
"lemma_FStar.UInt.pow2_values", "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.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"f5903426ed47b2327efd72b3f83419f5"
],
[
"Spec.Agile.HPKE.auth_encap",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"data_typing_intro_Spec.Agile.DH.DH_Curve448@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@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_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Agile.AEAD.algorithm",
"equation_Spec.Agile.DH.size_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.ciphersuite",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"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_99d574bfd1d8eaa5fe4d7c6d446fa884",
"refinement_interpretation_Tm_refine_b59543e631ac6b7ceb3db870f1176101",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"b043d35a57097ac3dec6ed29f115ae58"
],
[
"Spec.Agile.HPKE.auth_decap",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@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.DH.size_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf", "int_inversion",
"lemma_FStar.UInt.pow2_values", "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.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"d82d3746d7a3056d4c288d8177e79f0b"
],
[
"Spec.Agile.HPKE.auth_decap",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@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.DH.size_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf", "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_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"8f214b29be944fb073f96afa819c501b"
],
[
"Spec.Agile.HPKE.default_pkI",
1,
0,
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,
"7db1d0ab51d3ed9799057f2879a18d48"
],
[
"Spec.Agile.HPKE.default_psk",
1,
0,
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,
"aafbbb25d3522401ffeb98c1cc92d9d5"
],
[
"Spec.Agile.HPKE.default_pskId",
1,
0,
1,
[ "@query" ],
0,
"e0e4349caf76ccb814d3f557f378a705"
],
[
"Spec.Agile.HPKE.build_context",
1,
0,
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,
"e5a0d3c7843de58b48fed0c062293d31"
],
[
"Spec.Agile.HPKE.build_context",
2,
0,
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,
"ab50bbef29d3e2992561a16dcf8ecb3b"
],
[
"Spec.Agile.HPKE.build_context",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W8",
"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.DH.DH_Curve448@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W8@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.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_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.algorithm",
"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",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_99d574bfd1d8eaa5fe4d7c6d446fa884",
"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.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.U8@tok"
],
0,
"c4e6047aace0845b8deecf3447c57fe4"
],
[
"Spec.Agile.HPKE.ks_derive",
1,
0,
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,
"aada164d4bf92a12876978459d1a5b7d"
],
[
"Spec.Agile.HPKE.ks_derive",
2,
0,
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,
"51c5fd1b57f85b6e6b6812653f7bb447"
],
[
"Spec.Agile.HPKE.ks_derive",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"bool_inversion", "constructor_distinct_FStar.Integers.W128",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Integers.Winfinite",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_FStar.Seq.Base.seq",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Prims.unit",
"constructor_distinct_Spec.AES.AES128",
"constructor_distinct_Spec.AES.AES256",
"constructor_distinct_Spec.Agile.AEAD.AES128_GCM",
"constructor_distinct_Spec.Agile.AEAD.AES256_GCM",
"constructor_distinct_Spec.Agile.AEAD.CHACHA20_POLY1305",
"constructor_distinct_Spec.Agile.Cipher.AES128",
"constructor_distinct_Spec.Agile.Cipher.AES256",
"constructor_distinct_Spec.Agile.Cipher.CHACHA20",
"data_typing_intro_Spec.Agile.DH.DH_Curve448@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_FStar.Integers.W128@tok",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@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.AES.AES256@tok",
"equality_tok_Spec.Agile.Cipher.AES128@tok",
"equality_tok_Spec.Agile.Cipher.AES256@tok",
"equality_tok_Spec.Agile.Cipher.CHACHA20@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.op_At_Bar", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.AES.key_size",
"equation_Spec.Agile.AEAD.algorithm",
"equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg",
"equation_Spec.Agile.AEAD.key_length",
"equation_Spec.Agile.AEAD.size_key",
"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.build_context",
"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.hash_of_cs",
"equation_Spec.Agile.HPKE.id_of_cs",
"equation_Spec.Agile.HPKE.id_of_mode",
"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_cs_identifier",
"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_mode_identifier",
"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.tuple3",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm",
"fuel_guarded_inversion_Spec.Hash.Definitions.hash_alg",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.__cache_version_number__",
"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", "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_3c6f335880cd1199c873ba053c707b1b",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_4d6c12d91ad48195cce7aa69db5924e9",
"refinement_interpretation_Tm_refine_4ebfd0e83376a15979ce8403ef0ca858",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0",
"refinement_interpretation_Tm_refine_889261280ac78161e61fb5281df9a8c1",
"refinement_interpretation_Tm_refine_99d574bfd1d8eaa5fe4d7c6d446fa884",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_b1ad91029171789e0c66dd561092f84e",
"refinement_interpretation_Tm_refine_c11da8e8f0f9c9cde0eb7f130251c352",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e2b45c7bb19eecebc754851bbc30c994",
"refinement_interpretation_Tm_refine_f1f3a6a6d3da045b35e7ba130c8b362a",
"refinement_interpretation_Tm_refine_fb77d4109290540100357b20e0a78486",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"refinement_kinding_Tm_refine_4ebfd0e83376a15979ce8403ef0ca858",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"typing_Lib.ByteSequence.nat_to_bytes_be",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.maxint",
"typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.v", "typing_Lib.Sequence.create",
"typing_Lib.Sequence.op_At_Bar", "typing_Lib.Sequence.to_seq",
"typing_Prims.pow2", "typing_Spec.AES.gf8", "typing_Spec.AES.irred",
"typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.hash_of_cs",
"typing_Spec.Agile.HPKE.id_of_cs",
"typing_Spec.Agile.HPKE.id_of_mode",
"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_cs_identifier",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.Agile.HPKE.size_mode_identifier",
"typing_Spec.Agile.HPKE.size_psk",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok", "unit_typing"
],
0,
"a484b511bb9cb8a4bf5fc9f6cca9c8c3"
],
[
"Spec.Agile.HPKE.setupBaseI",
1,
0,
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,
"a8db5164b373d7567114e7e75732ffd5"
],
[
"Spec.Agile.HPKE.setupBaseI",
2,
0,
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,
"ea502626ac5ef5177060a3c328d81cfa"
],
[
"Spec.Agile.HPKE.setupBaseI",
3,
0,
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,
"c945a6eaaefe5ae9e69ed00f08911d29"
],
[
"Spec.Agile.HPKE.setupBaseR",
1,
0,
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,
"a11498df84e23e0f06fc2cd993304201"
],
[
"Spec.Agile.HPKE.setupBaseR",
2,
0,
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,
"9845c47eac67dda58caa2f942f69d887"
],
[
"Spec.Agile.HPKE.setupBaseR",
3,
0,
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,
"a795a6ffa0ca4da2c3729a5f56da311c"
],
[
"Spec.Agile.HPKE.setupAuthI",
1,
0,
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,
"22b8b346bb349501fe9eea6cea3fc7fb"
],
[
"Spec.Agile.HPKE.setupAuthI",
2,
0,
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,
"21628c2ce5b21e0201b80bbe1f68a7d4"
],
[
"Spec.Agile.HPKE.setupAuthI",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@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_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.max_info",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "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.max_info",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"8ecd44c4ff9cb9581bdfe2759680722e"
],
[
"Spec.Agile.HPKE.setupAuthR",
1,
0,
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,
"45ccd498f56a52c62fa102eb7de0a159"
],
[
"Spec.Agile.HPKE.setupAuthR",
2,
0,
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,
"07a2dfec85510d7d468ed48401c6cf7e"
],
[
"Spec.Agile.HPKE.setupAuthR",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@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_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.max_info",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "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.max_info",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"51ef8c2cf434e9d778b1813f8d55869f"
],
[
"Spec.Agile.HPKE.setupAuthPSKI",
1,
0,
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,
"4d838c4ad5aa0906381a77ec2cf2c298"
],
[
"Spec.Agile.HPKE.setupAuthPSKI",
2,
0,
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,
"35350576bbb1f4d5d0771dad06e4cccb"
],
[
"Spec.Agile.HPKE.setupAuthPSKI",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@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_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.max_info",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "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.max_info",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"4637b02b886beb1acddeddddd7c087e3"
],
[
"Spec.Agile.HPKE.setupPSKAuthR",
1,
0,
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,
"b050af6bb79cfd88f1e51b5d5d8f2b8b"
],
[
"Spec.Agile.HPKE.setupPSKAuthR",
2,
0,
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,
"99345805e583d8e6402b3349654e34fd"
],
[
"Spec.Agile.HPKE.setupPSKAuthR",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Tm_unit",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@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_key",
"equation_Spec.Agile.DH.size_public",
"equation_Spec.Agile.HPKE.max_info",
"equation_Spec.Agile.HPKE.size_dh_key",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.GaloisField.gf", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "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.max_info",
"typing_Spec.Agile.HPKE.size_dh_key",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"19eb2045739e5eca0a9180160ee8c081"
],
[
"Spec.Agile.HPKE.sealBase",
1,
0,
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,
"11f6a0134d44e0436fdf6c0f5d6d7b2d"
],
[
"Spec.Agile.HPKE.sealBase",
2,
0,
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,
"06f5369624c259703a2fcdc6262a2181"
],
[
"Spec.Agile.HPKE.sealBase",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@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.size_key",
"equation_Spec.Agile.AEAD.uint8",
"equation_Spec.Agile.HPKE.aead_of_cs",
"equation_Spec.Agile.HPKE.key_aead_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_label_key",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.pow2_4", "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_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_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.Agile.HPKE.max_info",
"typing_Spec.Agile.HPKE.size_aead_nonce",
"typing_Spec.Agile.HPKE.size_label_key",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"bc49d20f9a16547ec031837a3e37604f"
],
[
"Spec.Agile.HPKE.openBase",
1,
0,
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,
"abd7df73ea82d68017057cf970b9b49c"
],
[
"Spec.Agile.HPKE.openBase",
2,
0,
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,
"149019d6282d917b1a147737384637eb"
],
[
"Spec.Agile.HPKE.openBase",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Spec.Agile.DH_pretyping_15dc3859637146b5b92c6f7bcd69a314",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W64",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"data_typing_intro_Spec.Agile.DH.DH_Curve448@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W64@tok",
"equality_tok_FStar.Integers.W8@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.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_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.algorithm",
"equation_Spec.Agile.AEAD.is_supported_alg",
"equation_Spec.Agile.AEAD.iv_length",
"equation_Spec.Agile.AEAD.max_length",
"equation_Spec.Agile.AEAD.size_key",
"equation_Spec.Agile.AEAD.size_tag",
"equation_Spec.Agile.AEAD.tag_length",
"equation_Spec.Agile.AEAD.uint8",
"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.max_info",
"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_aead_tag",
"equation_Spec.Agile.HPKE.size_dh_public",
"equation_Spec.Agile.HPKE.size_label_key",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.GaloisField.gf",
"equation_Spec.Hash.Definitions.algorithm",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"fuel_guarded_inversion_Spec.Agile.DH.algorithm",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.pow2_4", "primitive_Prims.op_Addition",
"primitive_Prims.op_LessThanOrEqual",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7087bb9f7385184591d10c61617cb0c4",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7eec435bed21a0f9089c1978e6ee3b8d",
"refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955",
"refinement_interpretation_Tm_refine_99d574bfd1d8eaa5fe4d7c6d446fa884",
"refinement_interpretation_Tm_refine_9b8b991835088c05805a568c0485d476",
"refinement_interpretation_Tm_refine_ba2b797d3e0211cc8daf210df7ba8624",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.size_tag",
"typing_Spec.Agile.HPKE.aead_of_cs",
"typing_Spec.Agile.HPKE.curve_of_cs",
"typing_Spec.Agile.HPKE.max_info",
"typing_Spec.Agile.HPKE.size_aead_nonce",
"typing_Spec.Agile.HPKE.size_dh_public",
"typing_Spec.Agile.HPKE.size_label_key",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"b2fa005b8b69e5ebe9bef159dc0dbabf"
]
]
]
Computing file changes ...
