[
  "Ò#€¬´4}ø'Gi\u000bØ—9;",
  [
    [
      "Vale.AES.AES_s.nk",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.AES.AES_s.AES_128",
        "disc_equation_Vale.AES.AES_s.AES_192",
        "disc_equation_Vale.AES.AES_s.AES_256",
        "fuel_guarded_inversion_Vale.AES.AES_s.algorithm"
      ],
      0,
      "8e7e07c3c67809088b4bff0a4a8681e1"
    ],
    [
      "Vale.AES.AES_s.nr",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Vale.AES.AES_s.AES_128",
        "disc_equation_Vale.AES.AES_s.AES_192",
        "disc_equation_Vale.AES.AES_s.AES_256",
        "fuel_guarded_inversion_Vale.AES.AES_s.algorithm"
      ],
      0,
      "b41cd1d888141cde450e0ff3f35b6d18"
    ],
    [
      "Vale.AES.AES_s.aes_key_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "lemma_FStar.Seq.Base.hasEq_lemma",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "a9e067f578d5a305fa5a935b8df87c89"
    ],
    [
      "Vale.AES.AES_s.aes_key",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "lemma_FStar.Seq.Base.hasEq_lemma",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "db3f36ed807e8087b0ec87f6386941fb"
    ],
    [
      "Vale.AES.AES_s.eval_rounds_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "binder_x_1bf7805dca102a20dd4cf40ee0e4c344_2",
        "binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_1",
        "binder_x_e97427d583e1f4d42a96b4bdd8dae147_0", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four", "int_inversion",
        "int_typing", "primitive_Prims.op_Equality",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_315a550f138cfdf4055c9a83a4f16559",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "ee70740fe5ad3bfc3c861308f822674c"
    ],
    [
      "Vale.AES.AES_s.eval_rounds_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "7970f844f22e5cf68e8905c3c0ff1301"
    ],
    [
      "Vale.AES.AES_s.eval_cipher_def",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_Vale.AES.AES_s.algorithm",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "ad2e22113474cf75cfa0567454e455b5"
    ],
    [
      "Vale.AES.AES_s.eval_cipher_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "5c08476b97edb6ff0b40ee114e344f4a"
    ],
    [
      "Vale.AES.AES_s.expand_key_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
        "binder_x_67f87028e6cd57438f0518e237aba197_1",
        "binder_x_6e081d3fd4c7d96421c0174a146dcfd4_2",
        "constructor_distinct_Tm_unit", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "equation_Vale.AES.AES_s.aes_key_LE",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_11cdebb45c0a0cca398f44b5f50276f4",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
        "refinement_interpretation_Tm_refine_b112e58e47b3662e31627d314f992310",
        "refinement_interpretation_Tm_refine_c5409a723e1541d8f07c4f0465ea1dd1",
        "typing_FStar.Seq.Base.length",
        "typing_tok_Vale.AES.AES_s.AES_128@tok",
        "well-founded-ordering-on-nat"
      ],
      0,
      "27b994fa2f98b27b051cb62d06abb460"
    ],
    [
      "Vale.AES.AES_s.expand_key_reveal",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Tm_unit",
        "disc_equation_Vale.AES.AES_s.AES_128",
        "disc_equation_Vale.AES.AES_s.AES_192",
        "disc_equation_Vale.AES.AES_s.AES_256", "eq2-interp",
        "equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "078f936f69d49287aa724a9371984503"
    ],
    [
      "Vale.AES.AES_s.key_schedule_to_round_keys",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
        "binder_x_d7643cb47c00f184cbfede60aad14863_1", "equation_Prims.nat",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_56fce1a01658afc5bf5db7dd799c58ab",
        "refinement_interpretation_Tm_refine_8675e80e2a8f9bda5210205b84b7bbbb",
        "typing_FStar.Seq.Base.create", "well-founded-ordering-on-nat"
      ],
      0,
      "9ea5880df41ec06eb2260b2705c7f408"
    ],
    [
      "Vale.AES.AES_s.key_to_round_keys_LE",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
        "eq2-interp", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.AES_s.nb", "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6111c4f6a61843caee0d07c84de0edb2",
        "refinement_interpretation_Tm_refine_dd592ff911d0f80cdf0ace6c4224ff73",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "7de2acd5a496764f91110a8d92db1939"
    ],
    [
      "Vale.AES.AES_s.aes_encrypt_LE_def",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "2950d82a07df201380278c88707e61ca"
    ],
    [
      "Vale.AES.AES_s.aes_encrypt_LE_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "06ce33dd115f926f2b1e2ee035189f7b"
    ],
    [
      "Vale.AES.AES_s.key_to_round_keys",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Vale.AES.AES_s.AES_128", "eq2-interp",
        "equation_Vale.AES.AES_s.aes_key",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "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.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "fuel_guarded_inversion_Vale.AES.AES_s.algorithm",
        "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",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
        "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c2a75a3c0618fe8966569957451b4eb6",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
      ],
      0,
      "f6928fd21716e81597488d3f9e0c2da8"
    ],
    [
      "Vale.AES.AES_s.aes_encrypt",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "eq2-interp",
        "equation_Vale.AES.AES_s.aes_key",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Words.Seq_s.seq16",
        "equation_Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "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",
        "fuel_guarded_inversion_Vale.AES.AES_s.algorithm",
        "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",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
        "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c2a75a3c0618fe8966569957451b4eb6",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
      ],
      0,
      "5501165770cef312e9d7deab795bbf57"
    ]
  ]
]