[ "EoÐñíAa–Ñ$ïgƒÀU¢", [ [ "Spec.Cipher.Expansion.cipher_alg_of_impl", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "disc_equation_Spec.Cipher.Expansion.Hacl_CHACHA20", "disc_equation_Spec.Cipher.Expansion.Vale_AES128", "disc_equation_Spec.Cipher.Expansion.Vale_AES256", "fuel_guarded_inversion_Spec.Cipher.Expansion.impl" ], 0, "4d1bdf2b30a45f5eca0f6cc461dc3f7f" ], [ "Spec.Cipher.Expansion.vale_alg_of_cipher_alg", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Spec.Agile.Cipher.AES128", "constructor_distinct_Spec.Agile.Cipher.AES256", "constructor_distinct_Spec.Agile.Cipher.CHACHA20", "disc_equation_Spec.Agile.Cipher.AES128", "disc_equation_Spec.Agile.Cipher.AES256", "equality_tok_Spec.Agile.Cipher.AES128@tok", "equality_tok_Spec.Agile.Cipher.AES256@tok", "fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg", "refinement_interpretation_Tm_refine_177c69f55dbc44094b230a6a570a50b1" ], 0, "a8ca3b50ec2431c1079c6b0df1c401a2" ], [ "Spec.Cipher.Expansion.vale_xkey_length", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Agile.Cipher.AES128", "constructor_distinct_Spec.Agile.Cipher.AES256", "disc_equation_Spec.Agile.Cipher.AES128", "disc_equation_Spec.Agile.Cipher.AES256", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Agile.Cipher.AES128@tok", "equality_tok_Spec.Agile.Cipher.AES256@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.Cipher.Expansion.vale_cipher_alg", "equation_Spec.GaloisField.gf", "lemma_FStar.UInt.pow2_values", "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_177c69f55dbc44094b230a6a570a50b1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "92f6783874c7abac43e8be755643e696" ], [ "Spec.Cipher.Expansion.vale_aes_expansion", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Prims.unit", "constructor_distinct_Spec.AES.AES128", "constructor_distinct_Spec.AES.AES256", "constructor_distinct_Spec.Agile.Cipher.AES128", "constructor_distinct_Spec.Agile.Cipher.AES256", "constructor_distinct_Tm_unit", "constructor_distinct_Vale.AES.AES_s.AES_128", "constructor_distinct_Vale.AES.AES_s.AES_192", "constructor_distinct_Vale.AES.AES_s.AES_256", "constructor_distinct_Vale.AES.AES_s.algorithm", "eq2-interp", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@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_Vale.AES.AES_s.AES_128@tok", "equality_tok_Vale.AES.AES_s.AES_256@tok", "equation_FStar.Seq.Properties.lseq", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.sec_int_t", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Spec.AES.aes_key", "equation_Spec.AES.elem", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.AES.key_size", "equation_Spec.Agile.Cipher.aes_alg_of_alg", "equation_Spec.Agile.Cipher.key", "equation_Spec.Chacha20.size_key", "equation_Spec.Cipher.Expansion.vale_alg_of_cipher_alg", "equation_Spec.Cipher.Expansion.vale_cipher_alg", "equation_Spec.Cipher.Expansion.vale_xkey_length", "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf", "equation_Vale.AES.AES_s.is_aes_key_LE", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE", "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.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "function_token_typing_Spec.AES.elem", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac", "refinement_interpretation_Tm_refine_177c69f55dbc44094b230a6a570a50b1", "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_edbbd4b08cd9cea42a702b654f23e518", "typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8", "typing_Spec.Cipher.Expansion.vale_alg_of_cipher_alg", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "typing_Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8", "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE", "unit_typing" ], 0, "ce50ce2886ef793d1cf92253dfce8721" ], [ "Spec.Cipher.Expansion.uu___29", 1, 0, 0, [ "@query" ], 0, "77cf65a5e7d650253944ce0280ae2172" ], [ "Spec.Cipher.Expansion.uu___30", 1, 0, 0, [ "@query" ], 0, "a9c50a72f041e969d41d378c16456b32" ], [ "Spec.Cipher.Expansion.xkey_length", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "disc_equation_Spec.Agile.Cipher.AES128", "disc_equation_Spec.Agile.Cipher.AES256", "disc_equation_Spec.Agile.Cipher.CHACHA20", "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.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Cipher.Expansion.uu___29", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Agile.Cipher.cipher_alg", "function_token_typing_Spec.Cipher.Expansion.uu___29", "inversion-interp", "lemma_FStar.UInt.pow2_values", "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_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "3df1c97146542bd7bbd46b4bbfabd3e4" ], [ "Spec.Cipher.Expansion.concrete_xkey_length", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "disc_equation_Spec.Cipher.Expansion.Hacl_CHACHA20", "disc_equation_Spec.Cipher.Expansion.Vale_AES128", "disc_equation_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.squash", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Cipher.Expansion.cipher_alg_of_impl", "equation_Spec.Cipher.Expansion.uu___30", "equation_Spec.Cipher.Expansion.vale_cipher_alg", "equation_Spec.GaloisField.gf", "fuel_guarded_inversion_Spec.Cipher.Expansion.impl", "function_token_typing_Spec.Cipher.Expansion.uu___30", "inversion-interp", "lemma_FStar.UInt.pow2_values", "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_177c69f55dbc44094b230a6a570a50b1", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8", "typing_Spec.Cipher.Expansion.vale_xkey_length", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Spec.Agile.Cipher.AES128@tok", "typing_tok_Spec.Agile.Cipher.AES256@tok" ], 0, "9405f40ecae64b9f7360ae5cdfb03f5e" ], [ "Spec.Cipher.Expansion.concrete_expand", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Spec.Agile.Cipher.CHACHA20", "constructor_distinct_Spec.Cipher.Expansion.Hacl_CHACHA20", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES128", "constructor_distinct_Spec.Cipher.Expansion.Vale_AES256", "disc_equation_Spec.Cipher.Expansion.Hacl_CHACHA20", "disc_equation_Spec.Cipher.Expansion.Vale_AES128", "disc_equation_Spec.Cipher.Expansion.Vale_AES256", "equality_tok_Spec.Agile.Cipher.AES128@tok", "equality_tok_Spec.Agile.Cipher.AES256@tok", "equality_tok_Spec.Agile.Cipher.CHACHA20@tok", "equality_tok_Spec.Cipher.Expansion.Hacl_CHACHA20@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES128@tok", "equality_tok_Spec.Cipher.Expansion.Vale_AES256@tok", "equation_Prims.squash", "equation_Spec.Agile.Cipher.key", "equation_Spec.Chacha20.key", "equation_Spec.Chacha20.size_key", "equation_Spec.Cipher.Expansion.cipher_alg_of_impl", "equation_Spec.Cipher.Expansion.concrete_xkey", "equation_Spec.Cipher.Expansion.concrete_xkey_length", "equation_Spec.Cipher.Expansion.uu___30", "fuel_guarded_inversion_Spec.Cipher.Expansion.impl", "function_token_typing_Spec.Cipher.Expansion.uu___30", "inversion-interp", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "9893ea085264cefc41b32bdb120fd916" ] ] ]