[
  "´\u0019u—Kí`·S\n;åãî`7",
  [
    [
      "Vale.AES.GCM.upper3_equal",
      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",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "a0518e36ddef3d1180fd94db5eda9c7d"
    ],
    [
      "Vale.AES.GCM.lower3_equal",
      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",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
      ],
      0,
      "c51a54dd221a25f4eadc5336f00f0257"
    ],
    [
      "Vale.AES.GCM.lemma_set_to_one_equality",
      1,
      1,
      0,
      [
        "@query", "equation_Vale.AES.GCM.set_to_one_LE",
        "equation_Vale.AES.GCM.upper3_equal",
        "equation_Vale.Def.Words.Four_s.four_insert",
        "equation_Vale.Def.Words_s.nat32", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0"
      ],
      0,
      "e55fe3ea592f63b6558a237db3aa1750"
    ],
    [
      "Vale.AES.GCM.lemma_set_to_one_reverse_equality",
      1,
      1,
      0,
      [
        "@query", "equation_Vale.AES.GCM.lower3_equal",
        "equation_Vale.AES.GCM.set_to_one_LE",
        "equation_Vale.Def.Words.Four_s.four_insert",
        "equation_Vale.Def.Words.Four_s.four_reverse",
        "equation_Vale.Def.Words_s.nat32", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1"
      ],
      0,
      "018ee6419b5b9c317456d2d4a0cd5ad4"
    ],
    [
      "Vale.AES.GCM.lemma_le_bytes_to_quad32_prefix_equality",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Vale.AES.GCM_interpretation_Tm_arrow_efe96bb9514bece12be080c2a3348ae5",
        "equation_Prims.nat", "equation_Vale.AES.GCM.lower3_equal",
        "equation_Vale.Def.Types_s.le_bytes_to_quad32_def",
        "equation_Vale.Def.Words.Seq_s.seq_to_four_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",
        "function_token_typing_Vale.Def.Types_s.le_bytes_to_quad32",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "interpretation_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
        "interpretation_Tm_abs_ad3ad425f83578beeb8ba014cbc730a3",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
        "refinement_interpretation_Tm_refine_528966909e656beff90629dc95073b2d",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_FStar.Seq.Base.index",
        "token_correspondence_Vale.Def.Types_s.le_bytes_to_quad32_def",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Tm_abs_9c9244fb918a1d2c4c278c71625bc17c",
        "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
      ],
      0,
      "20637132eb25f2632dd62af83859ea04"
    ],
    [
      "Vale.AES.GCM.lemma_le_seq_quad32_to_bytes_prefix_equality",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length"
      ],
      0,
      "3da43d453a10771502026c13cc8f27b5"
    ],
    [
      "Vale.AES.GCM.lemma_compute_iv_easy",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "kinding_Vale.Def.Words_s.four@tok",
        "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_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_FStar.Seq.Base.append"
      ],
      0,
      "f35eb29d68f48e67256b86fcd14ecb2f"
    ],
    [
      "Vale.AES.GCM.lemma_compute_iv_easy",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
        "equation_Vale.AES.GCM.lower3_equal",
        "equation_Vale.AES.GCM.set_to_one_LE",
        "equation_Vale.AES.GCM_s.compute_iv_BE_def",
        "equation_Vale.AES.GCM_s.supported_iv_LE",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Four_s.four_insert",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.AES.GCM_s.compute_iv_BE",
        "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_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_8f53c9bd715d5bf10798304ebe2c54e8",
        "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_Vale.AES.GCM_s.compute_iv_BE_def",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_Vale.Def.Types_s.le_quad32_to_bytes",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
      ],
      0,
      "fa0a8a5248f94663035d8ffc8f7a4031"
    ],
    [
      "Vale.AES.GCM.lemma_compute_iv_hard",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.AES.GCM_s.supported_iv_LE",
        "refinement_interpretation_Tm_refine_8f53c9bd715d5bf10798304ebe2c54e8"
      ],
      0,
      "26a5fbf716e490d86410abb2cc5efc4f"
    ],
    [
      "Vale.AES.GCM.lemma_compute_iv_hard",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.AES.GCM_s.compute_iv_BE_def",
        "equation_Vale.AES.GCM_s.supported_iv_LE",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Two_s.two_to_nat",
        "equation_Vale.Def.Words_s.nat1", "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.AES.GCM_s.compute_iv_BE",
        "function_token_typing_Vale.Def.Types_s.insert_nat64",
        "function_token_typing_Vale.Def.Types_s.insert_nat64_def",
        "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_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_Vale.Def.Words_s.Mktwo_hi",
        "projection_inverse_Vale.Def.Words_s.Mktwo_lo",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_8f53c9bd715d5bf10798304ebe2c54e8",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "token_correspondence_Vale.AES.GCM_s.compute_iv_BE_def",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "typing_Vale.Def.Words_s.int_to_natN"
      ],
      0,
      "b46010584fb9d8a9f4a44f5f9575287b"
    ],
    [
      "Vale.AES.GCM.gcm_encrypt_LE_fst_helper",
      1,
      1,
      0,
      [
        "@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_Tm_unit", "eq2-interp",
        "equation_FStar.Pervasives.Native.fst", "equation_Prims.nat",
        "equation_Prims.squash", "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.make_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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",
        "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", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
        "primitive_Prims.op_LessThan",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_Vale.AES.GCM_s.gcm_encrypt_LE_def",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.init",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "233ebc12451a2010efa999b04d63b8df"
    ],
    [
      "Vale.AES.GCM.gcm_encrypt_LE_snd_helper",
      1,
      1,
      0,
      [
        "@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_Tm_unit", "eq2-interp",
        "equation_FStar.Pervasives.Native.fst",
        "equation_FStar.Pervasives.Native.snd", "equation_Prims.nat",
        "equation_Prims.squash", "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.is_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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.Def.Words_s.four",
        "function_token_typing_Vale.AES.GCM_s.gcm_encrypt_LE",
        "function_token_typing_Vale.Def.Types_s.insert_nat64",
        "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", "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_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_06b9f0ab8ff3c0e49aa83954383f15a4",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_1c920df238056cce4004409123681721",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_Vale.AES.GCM_s.gcm_encrypt_LE_def",
        "token_correspondence_Vale.Def.Types_s.insert_nat64_def",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.AES.GCTR_s.pad_to_128_bits",
        "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_four_to_seq_LE"
      ],
      0,
      "0b106249266e56de4baaf47261a33e86"
    ],
    [
      "Vale.AES.GCM.gcm_blocks_helper_enc",
      1,
      1,
      0,
      [
        "@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_Tm_unit",
        "constructor_distinct_Vale.AES.AES_s.AES_128", "eq2-interp",
        "equation_Prims.min", "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR.aes_encrypt_BE",
        "equation_Vale.AES.GCTR.gctr_partial_def",
        "equation_Vale.AES.GCTR.make_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_block",
        "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_nat32_to_seq_nat8_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.Def.Words_s.four",
        "function_token_typing_Vale.AES.GCTR.gctr_partial",
        "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", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_e7e807af1cf762a4b6edbe15a1dc3944",
        "token_correspondence_Vale.AES.GCTR.gctr_partial_def",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.init",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "8a2866fe4838ade34ebe4b7adcde6244"
    ],
    [
      "Vale.AES.GCM.slice_append_back",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
        "bool_typing", "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Prims.squash", "int_inversion", "int_typing",
        "l_and-interp", "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_c2f575b3d23d23189e5d12bd5a9e4337",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length"
      ],
      0,
      "b2dd32b2cbf36ef6fd513957800891a1"
    ],
    [
      "Vale.AES.GCM.append_distributes_le_seq_quad32_to_bytes",
      1,
      1,
      0,
      [
        "@query", "equation_FStar.Seq.Base.op_At_Bar",
        "equation_Vale.Def.Words_s.nat8"
      ],
      0,
      "a6c4c33f21b25a31347da9ee6dd9fb94"
    ],
    [
      "Vale.AES.GCM.pad_to_128_bits_multiple_append",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length"
      ],
      0,
      "6e5334de9c2a38a91fc09afba399d3a6"
    ],
    [
      "Vale.AES.GCM.gcm_blocks_helper",
      1,
      1,
      0,
      [
        "@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_Tm_unit",
        "constructor_distinct_Vale.AES.AES_s.AES_128", "eq2-interp",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR.aes_encrypt_BE",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_block",
        "equation_Vale.AES.GCTR_s.inc32",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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.Def.Words_s.four",
        "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", "l_and-interp",
        "lemma_FStar.Seq.Base.hasEq_lemma",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_06b9f0ab8ff3c0e49aa83954383f15a4",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_1c920df238056cce4004409123681721",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.AES.GCTR_s.pad_to_128_bits",
        "typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Def.Types_s.quad32",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0"
      ],
      0,
      "ba307528dd2901df44e0773c2006856c"
    ],
    [
      "Vale.AES.GCM.lemma_length_simplifier",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "eq2-interp",
        "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "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_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.Seq.Base.append",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
      ],
      0,
      "f422e09c9d85e0f0c71ef267139b0598"
    ],
    [
      "Vale.AES.GCM.lemma_length_simplifier",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing", "eq2-interp",
        "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "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_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.Seq.Base.append",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
      ],
      0,
      "20df04268b3c401e0d8ef24353efa1ce"
    ],
    [
      "Vale.AES.GCM.gcm_blocks_helper_simplified",
      1,
      1,
      0,
      [
        "@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_Tm_unit",
        "data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "eq2-interp",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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.Def.Words_s.four",
        "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", "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.Seq.Base.lemma_len_slice",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_06b9f0ab8ff3c0e49aa83954383f15a4",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_1c920df238056cce4004409123681721",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.AES.GCTR_s.pad_to_128_bits",
        "typing_Vale.Def.Types_s.insert_nat64",
        "typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "fe5e550bae0cc5df3c47dd7336766f4c"
    ],
    [
      "Vale.AES.GCM.gcm_blocks_helper_simplified",
      2,
      1,
      0,
      [
        "@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_Tm_unit", "eq2-interp", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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.Def.Words_s.four",
        "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", "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.Seq.Base.lemma_len_slice",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_06b9f0ab8ff3c0e49aa83954383f15a4",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.AES.GCTR_s.pad_to_128_bits",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "1cec947e58c30ee395bfac801381748f"
    ],
    [
      "Vale.AES.GCM.lemma_gcm_encrypt_decrypt_equiv",
      1,
      1,
      0,
      [
        "@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_Tm_unit", "eq2-interp", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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",
        "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", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "1e467443949ce69c0d24c573e998529e"
    ],
    [
      "Vale.AES.GCM.lemma_gcm_encrypt_decrypt_equiv",
      2,
      1,
      0,
      [
        "@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_Tm_unit", "eq2-interp",
        "equation_FStar.Pervasives.Native.fst", "equation_Prims.nat",
        "equation_Prims.squash", "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.GCM_s.gcm_encrypt_LE_def",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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",
        "function_token_typing_Vale.AES.GCM_s.gcm_decrypt_LE",
        "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", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_init_len", "primitive_Prims.op_LessThan",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_Vale.AES.GCM_s.gcm_decrypt_LE_def",
        "token_correspondence_Vale.AES.GCM_s.gcm_encrypt_LE_def",
        "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "4689f9ef5e61707fd1919eccbc4f8633"
    ],
    [
      "Vale.AES.GCM.gcm_blocks_helper_dec_simplified",
      1,
      1,
      0,
      [
        "@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_Tm_unit", "eq2-interp", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "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_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.init",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "9547146827f72c054f7858aff6c69cd3"
    ],
    [
      "Vale.AES.GCM.gcm_blocks_helper_dec_simplified",
      2,
      1,
      0,
      [
        "@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_Tm_unit", "eq2-interp", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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.Def.Words_s.four",
        "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", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.init",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "abe61e6ff8d76a0d3339be37709be66f"
    ],
    [
      "Vale.AES.GCM.gcm_decrypt_LE_tag",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "eq2-interp", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "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.nat1", "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_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_create_len",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0fe8a12189cf4c417dda723cc135a9ac",
        "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.length",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
      ],
      0,
      "c0fa7c6966829bd8cdd45780d0129849"
    ],
    [
      "Vale.AES.GCM.gcm_blocks_dec_helper",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "constructor_distinct_Tm_unit", "eq2-interp",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCM.gcm_decrypt_LE_tag",
        "equation_Vale.AES.GCTR.aes_encrypt_BE",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_block",
        "equation_Vale.AES.GCTR_s.inc32",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones",
        "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "l_and-interp", "lemma_FStar.Seq.Base.hasEq_lemma",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_eq_refl",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_FStar.UInt.pow2_values",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "lemma_Vale.Def.Words.Seq.seq_nat8_to_seq_nat32_to_seq_nat8_LE",
        "lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi2",
        "proj_equation_Vale.Def.Words_s.Mkfour_hi3",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_06b9f0ab8ff3c0e49aa83954383f15a4",
        "refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_1c920df238056cce4004409123681721",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.AES.GCTR_s.pad_to_128_bits",
        "typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Def.Types_s.quad32",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Math.Poly2.Bits.of_nat32",
        "typing_Vale.Math.Poly2_s.degree"
      ],
      0,
      "3ace9e8fe028e0b55498c8fc24ff43f5"
    ],
    [
      "Vale.AES.GCM.gcm_blocks_dec_helper_simplified",
      1,
      1,
      0,
      [
        "@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_Tm_unit",
        "data_typing_intro_Vale.Def.Words_s.Mkfour@tok", "eq2-interp",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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.Def.Words_s.four",
        "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", "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.Seq.Base.lemma_len_slice",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_06b9f0ab8ff3c0e49aa83954383f15a4",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_1c920df238056cce4004409123681721",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.AES.GCTR_s.pad_to_128_bits",
        "typing_Vale.Def.Types_s.insert_nat64",
        "typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "7e39019038c05f181fea471f72829015"
    ],
    [
      "Vale.AES.GCM.gcm_blocks_dec_helper_simplified",
      2,
      1,
      0,
      [
        "@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_Tm_unit", "eq2-interp", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Vale.AES.AES_s.is_aes_key",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_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.Def.Words_s.four",
        "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", "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.Seq.Base.lemma_len_slice",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_06b9f0ab8ff3c0e49aa83954383f15a4",
        "refinement_interpretation_Tm_refine_12cfdc5e5e9b4a21e137c684eae73d5b",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.AES.GCTR_s.pad_to_128_bits",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE"
      ],
      0,
      "46b927408cd8cddc8c1f95e021181de8"
    ],
    [
      "Vale.AES.GCM.decrypt_helper",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "l_and-interp", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "2dd1934caa4af966ebd459b1c95ec85a"
    ],
    [
      "Vale.AES.GCM.decrypt_helper",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_typing", "equation_FStar.Pervasives.Native.snd",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.GCM.gcm_decrypt_LE_tag",
        "equation_Vale.AES.GCM_s.gcm_decrypt_LE_def",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.AES.GCM_s.gcm_decrypt_LE",
        "function_token_typing_Vale.Def.Types_s.insert_nat64",
        "int_inversion", "l_and-interp", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThan",
        "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "token_correspondence_Vale.AES.GCM_s.gcm_decrypt_LE_def",
        "token_correspondence_Vale.Def.Types_s.insert_nat64_def"
      ],
      0,
      "54587ca58536ceaec0474f6a009e4545"
    ]
  ]
]