[ "Ȇø¨_6å:9«•\u0014dfWÕ", [ [ "Spec.Agile.AEAD.uu___2", 1, 2, 1, [ "@query" ], 0, "c537298961be8964e4ac88a179311860" ], [ "Spec.Agile.AEAD.cipher_alg_of_supported_alg", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "disc_equation_Spec.Agile.AEAD.AES128_GCM", "disc_equation_Spec.Agile.AEAD.AES256_GCM", "disc_equation_Spec.Agile.AEAD.CHACHA20_POLY1305", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.supported_alg", "refinement_interpretation_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0", "typing_Spec.Agile.AEAD.is_supported_alg" ], 0, "634f66c0078621b4532ad8c279e86147" ], [ "Spec.Agile.AEAD.key_length", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "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", "disc_equation_Spec.Agile.AEAD.AES128_CCM", "disc_equation_Spec.Agile.AEAD.AES128_CCM8", "disc_equation_Spec.Agile.AEAD.AES128_GCM", "disc_equation_Spec.Agile.AEAD.AES256_CCM", "disc_equation_Spec.Agile.AEAD.AES256_CCM8", "disc_equation_Spec.Agile.AEAD.AES256_GCM", "disc_equation_Spec.Agile.AEAD.CHACHA20_POLY1305", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Agile.AEAD.alg", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.is_supported_alg", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Spec.Agile.AEAD.AES256_GCM@tok", "typing_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok" ], 0, "5b9c837edcfd78a524e15f51c5033528" ], [ "Spec.Agile.AEAD.tag_length", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "disc_equation_Spec.Agile.AEAD.AES128_CCM", "disc_equation_Spec.Agile.AEAD.AES128_CCM8", "disc_equation_Spec.Agile.AEAD.AES128_GCM", "disc_equation_Spec.Agile.AEAD.AES256_CCM", "disc_equation_Spec.Agile.AEAD.AES256_CCM8", "disc_equation_Spec.Agile.AEAD.AES256_GCM", "disc_equation_Spec.Agile.AEAD.CHACHA20_POLY1305", "fuel_guarded_inversion_Spec.Agile.AEAD.alg" ], 0, "e726595ec7f028bc8fe4e9393257fc12" ], [ "Spec.Agile.AEAD.iv_length", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_FStar.Integers.Signed", "constructor_distinct_FStar.Integers.W128", "constructor_distinct_FStar.Integers.Winfinite", "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.W128@tok", "equality_tok_FStar.Integers.Winfinite@tok", "equation_FStar.Integers.width_of_sw", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.supported_alg", "projection_inverse_FStar.Integers.Signed__0", "refinement_interpretation_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0", "typing_Spec.Agile.AEAD.is_supported_alg" ], 0, "98206bdb6cd90bdef0fd681df3c3c1f3" ], [ "Spec.Agile.AEAD.max_length", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "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.U32", "constructor_distinct_Lib.IntTypes.U8", "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.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.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.supported_alg", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "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_ce5a1bd8437baa640019cd70bf466fc0", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.is_supported_alg", "typing_Spec.Agile.AEAD.uu___is_AES256_GCM", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key" ], 0, "fbb39b5f574978dba50e616b157e67dd" ], [ "Spec.Agile.AEAD.lbytes", 1, 2, 1, [ "@query" ], 0, "74fdcf76a48b58e9a48b0f844f24491c" ], [ "Spec.Agile.AEAD.vale_alg_of_alg", 1, 0, 0, [ "@query", "assumption_Spec.Agile.AEAD.alg__uu___haseq" ], 0, "55d2ed1aaed99557a593af5fc6c4bfde" ], [ "Spec.Agile.AEAD.vale_alg_of_alg", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Spec.Agile.AEAD.AES128_GCM", "constructor_distinct_Spec.Agile.AEAD.AES256_GCM", "disc_equation_Spec.Agile.AEAD.AES128_GCM", "disc_equation_Spec.Agile.AEAD.AES256_GCM", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "refinement_interpretation_Tm_refine_5171614844d45d48a27a076e659221d2" ], 0, "e17307a5fd6436938a4a0eefb3519d8b" ], [ "Spec.Agile.AEAD.gcm_encrypt_tag_length", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Def.Types_s_interpretation_Tm_arrow_f33a1e80d097b65957309e13d3848492", "b2t_def", "constructor_distinct_FStar.Integers.W16", "constructor_distinct_FStar.Integers.W32", "constructor_distinct_FStar.Integers.W8", "constructor_distinct_FStar.Integers.Winfinite", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S64", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.AES.AES_s.AES_128", "constructor_distinct_Vale.AES.AES_s.AES_192", "constructor_distinct_Vale.AES.AES_s.AES_256", "data_elim_FStar.Pervasives.Native.Mktuple2", "data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "eq2-interp", "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.U8@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "equation_Vale.AES.AES_s.aes_key_LE", "equation_Vale.AES.AES_s.is_aes_key", "equation_Vale.AES.AES_s.is_aes_key_LE", "equation_Vale.AES.GCM_s.gcm_encrypt_LE_def", "equation_Vale.AES.GCTR_s.gctr_plain_LE", "equation_Vale.AES.GCTR_s.is_gctr_plain_LE", "equation_Vale.AES.GCTR_s.pad_to_128_bits", "equation_Vale.AES.GHash_s.ghash_plain_LE", "equation_Vale.Def.Types_s.insert_nat64_def", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "fuel_guarded_inversion_Vale.AES.AES_s.algorithm", "function_token_typing_Vale.AES.GCM_s.gcm_encrypt_LE", "function_token_typing_Vale.Def.Types_s.reverse_bytes_quad32", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2", "lemma_Vale.AES.GCTR.gctr_encrypt_length", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "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__2", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_06b9f0ab8ff3c0e49aa83954383f15a4", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_1c920df238056cce4004409123681721", "refinement_interpretation_Tm_refine_27cb8547ad2b1e854c0d481d51e2247a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_3cde0f73125500a52bff30114a1a1137", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9516cded170631b955b6abc241ba7c49", "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1", "token_correspondence_Prims.pow2.fuel_instrumented", "token_correspondence_Vale.AES.GCM_s.gcm_encrypt_LE_def", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.AES.AES_s.aes_encrypt_LE", "typing_Vale.AES.GCM_s.compute_iv_BE", "typing_Vale.AES.GCM_s.gcm_encrypt_LE", "typing_Vale.AES.GCTR_s.pad_to_128_bits", "typing_Vale.AES.GHash_s.ghash_LE", "typing_Vale.Def.Types_s.insert_nat64_def", "typing_Vale.Def.Types_s.le_bytes_to_seq_quad32", "typing_Vale.Def.Types_s.le_quad32_to_bytes", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "84a793b6c5ae5884e54f05946ae781e1" ], [ "Spec.Agile.AEAD.gcm_encrypt_cipher_length", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.AES.AES_s.AES_128", "constructor_distinct_Vale.AES.AES_s.AES_192", "constructor_distinct_Vale.AES.AES_s.AES_256", "data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "eq2-interp", "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.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "equation_Vale.AES.AES_s.aes_key_LE", "equation_Vale.AES.AES_s.is_aes_key", "equation_Vale.AES.AES_s.is_aes_key_LE", "equation_Vale.AES.GCM_s.gcm_encrypt_LE_def", "equation_Vale.AES.GCTR_s.gctr_plain_LE", "equation_Vale.AES.GCTR_s.inc32", "equation_Vale.AES.GCTR_s.is_gctr_plain_LE", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "fuel_guarded_inversion_Vale.AES.AES_s.algorithm", "function_token_typing_Prims.int", "function_token_typing_Vale.AES.GCM_s.gcm_encrypt_LE", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_Lib.IntTypes.pow2_2", "lemma_Vale.AES.GCTR.gctr_encrypt_length", "primitive_Prims.op_LessThan", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_27cb8547ad2b1e854c0d481d51e2247a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1", "token_correspondence_Prims.pow2.fuel_instrumented", "token_correspondence_Vale.AES.GCM_s.gcm_encrypt_LE_def", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.AES.AES_s.aes_encrypt_LE", "typing_Vale.AES.GCM_s.compute_iv_BE", "typing_Vale.AES.GCTR_s.inc32", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "e4fbe2e64a54012b46765ec30203d8f5" ], [ "Spec.Agile.AEAD.encrypt", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "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.PUB", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S64", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U1", "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.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", "constructor_distinct_Vale.AES.AES_s.AES_128", "constructor_distinct_Vale.AES.AES_s.AES_256", "disc_equation_Spec.Agile.AEAD.AES128_GCM", "disc_equation_Spec.Agile.AEAD.AES256_GCM", "disc_equation_Spec.Agile.AEAD.CHACHA20_POLY1305", "eq2-interp", "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.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.AES.AES128@tok", "equality_tok_Spec.AES.AES256@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.Cipher.AES128@tok", "equality_tok_Spec.Agile.Cipher.AES256@tok", "equality_tok_Spec.Agile.Cipher.CHACHA20@tok", "equality_tok_Vale.AES.AES_s.AES_128@tok", "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.AES.key_size", "equation_Spec.Agile.AEAD.ad", "equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg", "equation_Spec.Agile.AEAD.cipher_length", "equation_Spec.Agile.AEAD.iv", "equation_Spec.Agile.AEAD.iv_length", "equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.kv", "equation_Spec.Agile.AEAD.lbytes", "equation_Spec.Agile.AEAD.max_length", "equation_Spec.Agile.AEAD.plain", "equation_Spec.Agile.AEAD.tag_length", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.AEAD.vale_alg_of_alg", "equation_Spec.Agile.Cipher.aes_alg_of_alg", "equation_Spec.Agile.Cipher.key_length", "equation_Spec.Chacha20.size_block", "equation_Spec.Chacha20.size_key", "equation_Spec.Chacha20Poly1305.size_block", "equation_Spec.Chacha20Poly1305.size_key", "equation_Spec.Chacha20Poly1305.size_nonce", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "equation_Vale.AES.AES_s.is_aes_key", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8", "equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Spec.AES.elem", "function_token_typing_Vale.Def.Words_s.nat8", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.Seq.Base.lemma_len_append", "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_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_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_982fb3d3fec67274e50be352a80fb36e", "refinement_interpretation_Tm_refine_b19a1c83769dccbdda4cf44bd4e3d295", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_dd6b7c82943901495ce61ec2042328d2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8", "typing_Spec.Chacha20.size_block", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "7e1e6f9445e833e0d46160ebc764f613" ], [ "Spec.Agile.AEAD.gcm_decrypt_cipher_length", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def", "bool_typing", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Vale.AES.AES_s.AES_128", "constructor_distinct_Vale.AES.AES_s.AES_192", "constructor_distinct_Vale.AES.AES_s.AES_256", "data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "eq2-interp", "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.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype", "equation_Prims.l_and", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_key", "equation_Vale.AES.AES_s.aes_key_LE", "equation_Vale.AES.AES_s.is_aes_key", "equation_Vale.AES.AES_s.is_aes_key_LE", "equation_Vale.AES.GCM_s.gcm_decrypt_LE_def", "equation_Vale.AES.GCTR_s.gctr_plain_LE", "equation_Vale.AES.GCTR_s.inc32", "equation_Vale.AES.GCTR_s.is_gctr_plain_LE", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "fuel_guarded_inversion_Vale.AES.AES_s.algorithm", "function_token_typing_Prims.int", "function_token_typing_Vale.AES.GCM_s.gcm_decrypt_LE", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_Lib.IntTypes.pow2_2", "lemma_Vale.AES.GCTR.gctr_encrypt_length", "primitive_Prims.op_LessThan", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_27cb8547ad2b1e854c0d481d51e2247a", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1", "token_correspondence_Prims.pow2.fuel_instrumented", "token_correspondence_Vale.AES.GCM_s.gcm_decrypt_LE_def", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.AES.AES_s.aes_encrypt_LE", "typing_Vale.AES.GCM_s.compute_iv_BE", "typing_Vale.AES.GCTR_s.inc32", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "f7b04d3998e60a520cc633cfffab4a11" ], [ "Spec.Agile.AEAD.decrypt", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_inversion", "constructor_distinct_FStar.Integers.Signed", "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.PUB", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S64", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U1", "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.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", "constructor_distinct_Vale.AES.AES_s.AES_128", "constructor_distinct_Vale.AES.AES_s.AES_256", "disc_equation_Spec.Agile.AEAD.AES128_GCM", "disc_equation_Spec.Agile.AEAD.AES256_GCM", "disc_equation_Spec.Agile.AEAD.CHACHA20_POLY1305", "eq2-interp", "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.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.AES.AES128@tok", "equality_tok_Spec.AES.AES256@tok", "equality_tok_Spec.Agile.AEAD.AES128_GCM@tok", "equality_tok_Spec.Agile.AEAD.AES256_GCM@tok", "equality_tok_Spec.Agile.AEAD.CHACHA20_POLY1305@tok", "equality_tok_Spec.Agile.Cipher.AES128@tok", "equality_tok_Spec.Agile.Cipher.AES256@tok", "equality_tok_Spec.Agile.Cipher.CHACHA20@tok", "equality_tok_Vale.AES.AES_s.AES_128@tok", "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_FStar.Integers.int_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.byte_t", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.AES.key_size", "equation_Spec.Agile.AEAD.ad", "equation_Spec.Agile.AEAD.cipher", "equation_Spec.Agile.AEAD.cipher_alg_of_supported_alg", "equation_Spec.Agile.AEAD.cipher_length", "equation_Spec.Agile.AEAD.is_supported_alg", "equation_Spec.Agile.AEAD.iv", "equation_Spec.Agile.AEAD.iv_length", "equation_Spec.Agile.AEAD.key_length", "equation_Spec.Agile.AEAD.kv", "equation_Spec.Agile.AEAD.lbytes", "equation_Spec.Agile.AEAD.max_length", "equation_Spec.Agile.AEAD.supported_alg", "equation_Spec.Agile.AEAD.tag_length", "equation_Spec.Agile.AEAD.uint8", "equation_Spec.Agile.AEAD.vale_alg_of_alg", "equation_Spec.Agile.Cipher.aes_alg_of_alg", "equation_Spec.Agile.Cipher.key_length", "equation_Spec.Chacha20.size_block", "equation_Spec.Chacha20.size_key", "equation_Spec.Chacha20Poly1305.size_block", "equation_Spec.Chacha20Poly1305.size_key", "equation_Spec.Chacha20Poly1305.size_nonce", "equation_Spec.Chacha20Poly1305.size_tag", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.size_block", "equation_Spec.Poly1305.size_key", "equation_Vale.AES.AES_s.is_aes_key", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8", "equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "function_token_typing_Lib.IntTypes.byte_t", "function_token_typing_Lib.IntTypes.uint8", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Spec.AES.elem", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.Seq.Base.lemma_len_slice", "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_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_1cc41c3630856663dcfa11216c896f06", "refinement_interpretation_Tm_refine_2a5baaeccb6b50d92d793d09091c6346", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_90a1661541e4f009452ab107b47b5955", "refinement_interpretation_Tm_refine_982fb3d3fec67274e50be352a80fb36e", "refinement_interpretation_Tm_refine_b19a1c83769dccbdda4cf44bd4e3d295", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_ce5a1bd8437baa640019cd70bf466fc0", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_dd6b7c82943901495ce61ec2042328d2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.Sequence.length", "typing_Spec.AES.gf8", "typing_Spec.Agile.AEAD.is_supported_alg", "typing_Spec.Agile.AEAD.tag_length", "typing_Spec.Chacha20.size_block", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Spec.Poly1305.size_key", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_Lib.IntTypes.U8@tok" ], 0, "5783494ca20f69d54a4fdd312d0bbebd" ], [ "Spec.Agile.AEAD.correctness", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Spec.Agile.AEAD.cipher_length", "equation_Spec.Agile.AEAD.encrypted", "equation_Spec.Agile.AEAD.max_length", "equation_Spec.Agile.AEAD.plain", "equation_Spec.Agile.AEAD.tag_length", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_9315e6f2e6143f3996b9238ef3ae182b", "refinement_interpretation_Tm_refine_b19a1c83769dccbdda4cf44bd4e3d295", "typing_Spec.Agile.AEAD.encrypt" ], 0, "cf4a9d64d72328ed32d7b0708404a976" ] ] ]