[
  "\u0006o蘩_繾演四郔碉U",
  [
    [
      "Vale.AES.GCTR.inc32lite",
      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.natN",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0"
      ],
      0,
      "7eea74d5abdcc4cea7124d0703db29d4"
    ],
    [
      "Vale.AES.GCTR.lemma_counter_init",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.BitVector.logand_vec.fuel_instrumented",
        "@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
        "@fuel_correspondence_FStar.UInt.to_vec.fuel_instrumented",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
        "bool_inversion", "bool_typing", "equation_FStar.BitVector.bv_t",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.logand",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.mod", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Vale.Arch.Types.lo64_def",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Four_s.four_to_two_two",
        "equation_Vale.Def.Words.Two_s.two_select",
        "equation_Vale.Def.Words.Two_s.two_to_nat",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
        "equation_Vale.Def.Words_s.natN",
        "equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
        "equation_with_fuel_FStar.UInt.to_vec.fuel_instrumented",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Prims.bool",
        "function_token_typing_Vale.Arch.Types.lo64",
        "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",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "proj_equation_Vale.Def.Words_s.Mktwo_lo",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_e2d5d62a90ceed8a6faf9d20615f4e1e",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "token_correspondence_FStar.UInt.to_vec.fuel_instrumented",
        "token_correspondence_Vale.Arch.Types.lo64_def",
        "typing_FStar.BitVector.logand_vec", "typing_FStar.Seq.Base.create",
        "typing_FStar.UInt.fits", "typing_FStar.UInt.to_vec",
        "typing_Prims.pow2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1",
        "typing_Vale.Def.Words_s.int_to_natN"
      ],
      0,
      "f9438f9e6a80a8e3b837e523eaebe00a"
    ],
    [
      "Vale.AES.GCTR.partial_seq_agreement",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000"
      ],
      0,
      "a3d679e925e04c243d57d1cca27b7e30"
    ],
    [
      "Vale.AES.GCTR.gctr_encrypt_block_offset",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "734574b5b154f2bdc784ddd35a0aceaa"
    ],
    [
      "Vale.AES.GCTR.gctr_encrypt_block_offset",
      2,
      1,
      0,
      [
        "@query", "equation_Vale.AES.GCTR_s.gctr_encrypt_block",
        "equation_Vale.AES.GCTR_s.inc32", "equation_Vale.Def.Words_s.nat32",
        "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_BoxInt_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,
      "cecc2e8c7900d9426448eabaea8a3e5f"
    ],
    [
      "Vale.AES.GCTR.gctr_encrypt_empty",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR.make_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "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",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "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_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
      ],
      0,
      "766554799338a08e9f65ee0d561cc37e"
    ],
    [
      "Vale.AES.GCTR.gctr_encrypt_empty",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE",
        "equation_Vale.AES.GCTR.make_gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_LE_def",
        "equation_Vale.AES.GCTR_s.gctr_plain_internal_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.Lib.Seqs_s.compose",
        "equation_Vale.Lib.Seqs_s.seq_map",
        "equation_with_fuel_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.AES.GCTR_s.gctr_encrypt_LE",
        "function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
        "interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
        "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_7ecc9ff2104c1b3467333d052c1b37c3",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
        "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_LE_def",
        "typing_FStar.Seq.Base.empty", "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_nat8_to_seq_nat32_LE",
        "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
      ],
      0,
      "55efa00fe456e82945f6da453147a565"
    ],
    [
      "Vale.AES.GCTR.aes_encrypt_BE",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "f8fbd26b5e9753eb59d587860a4ada05"
    ],
    [
      "Vale.AES.GCTR.gctr_registers_def",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "2f7ed559b8c6b63ad208afdddd5a31c9"
    ],
    [
      "Vale.AES.GCTR.gctr_registers_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "b50c651ed7bbb5df374ef22af49d1d63"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000"
      ],
      0,
      "86ff942833e21a5d7b03aa61c8678f9f"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "e9db59c3a9ec69e2924162c6f8b6795e"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_opaque_init",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.min",
        "equation_Vale.AES.GCTR.gctr_partial_def",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.AES.GCTR.gctr_partial",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxInt_proj_0",
        "token_correspondence_Vale.AES.GCTR.gctr_partial_def"
      ],
      0,
      "e9f35f0c8f3ac509b4390f713c23d67d"
    ],
    [
      "Vale.AES.GCTR.lemma_gctr_partial_append",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.min",
        "equation_Prims.nat", "equation_Vale.AES.GCTR.gctr_partial",
        "equation_Vale.AES.GCTR.gctr_partial_opaque",
        "equation_Vale.AES.GCTR_s.inc32", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Opaque_s.make_opaque",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "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_BoxInt_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",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_Vale.AES.GCTR.gctr_partial"
      ],
      0,
      "60f854c8d17befbf4b86599d49ab726d"
    ],
    [
      "Vale.AES.GCTR.lemma_gctr_partial_append",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.min",
        "equation_Prims.nat", "equation_Vale.AES.GCTR.gctr_partial_def",
        "equation_Vale.AES.GCTR_s.inc32", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.AES.GCTR.gctr_partial",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "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_BoxInt_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",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_Vale.AES.GCTR.gctr_partial_def"
      ],
      0,
      "757aa8869a93c0ff4c0ad2296a3b246b"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_opaque_ignores_postfix",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.min",
        "equation_Prims.nat", "equation_Vale.AES.GCTR.gctr_partial",
        "equation_Vale.AES.GCTR.gctr_partial_opaque",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Opaque_s.make_opaque",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_05a1a488a8ea9b2e17b311a5ff0bb8b1",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000",
        "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",
        "token_correspondence_Vale.AES.GCTR.gctr_partial"
      ],
      0,
      "1b737b17c410248610cba7540aebb322"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_opaque_ignores_postfix",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.min",
        "equation_Prims.nat", "equation_Vale.AES.GCTR.gctr_partial_def",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.AES.GCTR.gctr_partial",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "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_05a1a488a8ea9b2e17b311a5ff0bb8b1",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000",
        "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",
        "token_correspondence_Vale.AES.GCTR.gctr_partial_def",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "e841727f0d8c244723cd5ae0ce9cb8fb"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_extend6",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "9ec22f38fbf02dc3280e23cf2b73637f"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_extend6",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.min",
        "equation_Prims.nat", "equation_Vale.AES.GCTR.gctr_partial_def",
        "equation_Vale.AES.GCTR.inc32lite", "equation_Vale.AES.GCTR_s.inc32",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.AES.GCTR.gctr_partial",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "token_correspondence_Vale.AES.GCTR.gctr_partial_def",
        "typing_FStar.Seq.Base.length", "typing_Prims.min",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0"
      ],
      0,
      "ff7f6e123399f3173e7afd285da439d6"
    ],
    [
      "Vale.AES.GCTR.gctr_encrypt_recursive_length",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_e4836109f73687024ac3edd113084865",
        "binder_x_35779122094374fadf807bdd7bfc8013_2",
        "binder_x_ae567c2fb75be05905677af440075565_4",
        "binder_x_c3b8ca4826e9e8432a34e6824d62768b_3",
        "binder_x_e97427d583e1f4d42a96b4bdd8dae147_0",
        "binder_x_f960072d0bfae1e534f0393998cf6653_1",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.aes_key_LE",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_block",
        "equation_Vale.AES.GCTR_s.gctr_plain_internal_LE",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_with_fuel_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "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",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_Addition", "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_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.empty",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.head",
        "typing_Vale.AES.AES_s.aes_encrypt_LE",
        "typing_Vale.AES.GCTR_s.inc32", "typing_Vale.Def.Types_s.quad32_xor",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_tok_Prims.LexTop@tok", "well-founded-ordering-on-nat"
      ],
      0,
      "04df69a3967fa9deb44da1879cc897fa"
    ],
    [
      "Vale.AES.GCTR.gctr_encrypt_length",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.AES.AES_s.aes_key_LE",
        "equation_Vale.AES.GCTR_s.gctr_plain_LE",
        "refinement_interpretation_Tm_refine_27cb8547ad2b1e854c0d481d51e2247a",
        "refinement_interpretation_Tm_refine_465d996cbf22d32cb08a9b2aefd1ad7b",
        "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3"
      ],
      0,
      "874774d099ba7619731553dd685c1937"
    ],
    [
      "Vale.AES.GCTR.gctr_encrypt_length",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "@query",
        "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "binder_x_35779122094374fadf807bdd7bfc8013_2",
        "binder_x_63ff6bedd9b59ccc58bc7a6af3b47a72_1",
        "binder_x_c3b8ca4826e9e8432a34e6824d62768b_3",
        "binder_x_e97427d583e1f4d42a96b4bdd8dae147_0",
        "equation_FStar.Seq.Base.op_At_Bar",
        "equation_FStar.Seq.Properties.split", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.aes_key_LE",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_LE_def",
        "equation_Vale.AES.GCTR_s.gctr_plain_LE",
        "equation_Vale.AES.GCTR_s.gctr_plain_internal_LE",
        "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_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.Def.Words_s.four",
        "function_token_typing_Vale.AES.GCTR_s.gctr_encrypt_LE",
        "function_token_typing_Vale.Def.Types_s.le_bytes_to_seq_quad32",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_04f3daab46117a22c7e69935aa75c278",
        "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",
        "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_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "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_0fe8a12189cf4c417dda723cc135a9ac",
        "refinement_interpretation_Tm_refine_27cb8547ad2b1e854c0d481d51e2247a",
        "refinement_interpretation_Tm_refine_4541e819c92681ed9a776d05a593cda6",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_efdc432e922f5d070b4ab3b67fda1ef1",
        "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_LE_def",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Vale.AES.GCTR_s.gctr_encrypt_recursive",
        "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_nat8_to_seq_nat32_LE",
        "typing_Vale.Def.Words.Seq_s.seq_to_seq_four_LE"
      ],
      0,
      "2eb48cf38587714b6a553ef207c4408a"
    ],
    [
      "Vale.AES.GCTR.gctr_indexed_helper",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.AES.AES_s.aes_key_LE",
        "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3"
      ],
      0,
      "db28e5133025be0790495f376308dd60"
    ],
    [
      "Vale.AES.GCTR.gctr_indexed_helper",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_e4836109f73687024ac3edd113084865",
        "binder_x_35779122094374fadf807bdd7bfc8013_2",
        "binder_x_ae567c2fb75be05905677af440075565_4",
        "binder_x_c3b8ca4826e9e8432a34e6824d62768b_3",
        "binder_x_e97427d583e1f4d42a96b4bdd8dae147_0",
        "binder_x_f960072d0bfae1e534f0393998cf6653_1",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.aes_key_LE",
        "equation_Vale.AES.GCTR.aes_encrypt_BE",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_block",
        "equation_Vale.AES.GCTR_s.gctr_plain_internal_LE",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_with_fuel_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "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_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_index_create",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.AES.GCTR.gctr_encrypt_recursive_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Equality", "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_167ef714932ec832fb671890fc3eee6c",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_86acedbab4aa063aa52cf417ac3141b1",
        "refinement_interpretation_Tm_refine_8dd65c71dfe8b21be0b6480212d07c90",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_be84f82d45e5967648bfd92d64cb5eca",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f8caad6ddda489be07534c22db7d3ebb",
        "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Properties.head",
        "typing_Vale.AES.AES_s.aes_encrypt_LE",
        "typing_Vale.AES.GCTR_s.gctr_encrypt_block",
        "typing_Vale.AES.GCTR_s.inc32", "typing_Vale.Def.Types_s.quad32_xor",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_tok_Prims.LexTop@tok", "well-founded-ordering-on-nat"
      ],
      0,
      "c38b1f2f6106ba0dd399f56a7a7d7b1b"
    ],
    [
      "Vale.AES.GCTR.gctr_indexed",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.AES.AES_s.aes_key_LE",
        "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3"
      ],
      0,
      "6a393393f5eb99ec5fe3480ac282a219"
    ],
    [
      "Vale.AES.GCTR.gctr_indexed",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "@query", "binder_x_35779122094374fadf807bdd7bfc8013_2",
        "binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_4",
        "binder_x_c3b8ca4826e9e8432a34e6824d62768b_3",
        "binder_x_e97427d583e1f4d42a96b4bdd8dae147_0",
        "binder_x_f960072d0bfae1e534f0393998cf6653_1", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.aes_key_LE",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_16e48e2e4bd437230f03a1983752209d",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_55d9332cf0766ec1950e1203865a6be7",
        "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_Vale.AES.GCTR_s.gctr_encrypt_recursive"
      ],
      0,
      "580b2bbd961c888e74fb17f26be02e98"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_completed",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Vale.AES.GCTR.gctr_partial",
        "l_and-interp",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "084ae574269cb0f33ff439c9b7f68e90"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_completed",
      2,
      1,
      0,
      [
        "@query", "equation_Prims.min",
        "equation_Vale.AES.GCTR.gctr_partial_def"
      ],
      0,
      "0d019b89226f7f24fca4d5ef70cfc4c5"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_opaque_completed",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
        "equation_Prims.squash", "l_and-interp",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "bf0f650313265258edc549694155e9eb"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_opaque_completed",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.AES.GCTR.gctr_partial", "l_and-interp",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "token_correspondence_Vale.AES.GCTR.gctr_partial_def"
      ],
      0,
      "7bd5ce4ce55eb295e1f072f2dbf14dcf"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_to_full_basic",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE", "l_and-interp",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "2896ab69cc68134dba9a064c169f1564"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_to_full_basic",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_LE_def",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.AES.GCTR_s.gctr_encrypt_LE",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
        "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_LE_def"
      ],
      0,
      "3c680ad95ea354b0b0e353e8b3e6fc74"
    ],
    [
      "Vale.AES.GCTR.step1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Properties.split", "equation_Prims.nat",
        "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "equation_Vale.Def.Words_s.nat8",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_84a2905827f2440604f2654bb0f156ec",
        "refinement_interpretation_Tm_refine_86d33b0f21e34d7762468dcd4dbae48d",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "typing_FStar.Seq.Base.slice",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
      ],
      0,
      "6bd2b18bd52fa6c1d4436e2e6199add7"
    ],
    [
      "Vale.AES.GCTR.lemma_slice_orig_index",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "eq2-interp",
        "equation_Prims.nat", "equation_Prims.squash", "int_inversion",
        "l_and-interp", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c7f248c50d182c40aac9022fc9a66edc"
      ],
      0,
      "04695136081bf78e3e32f82d76613f8a"
    ],
    [
      "Vale.AES.GCTR.lemma_ishl_32",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "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_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "216be49f23e42ae8b821f8c26705d197"
    ],
    [
      "Vale.AES.GCTR.lemma_ishl_ixor_32",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_Prims.nat", "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
        "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_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "0e68411cdf548f773939193c578a7290"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise_1_helper1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "4b2f5333c18a91cdc2c650800849b8ba"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise_2_helper1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Words_s.nat16", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "6a046c2108c295ef2773f568b96814ee"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise_3_helper1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.AES.GCTR.nat24", "equation_Vale.Def.Words_s.natN",
        "int_inversion", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "2e52debe08ea9f69a2b0ede71a7dbe66"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise_1_helper2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_BoxInt_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",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Def.Words_s.int_to_natN"
      ],
      0,
      "adc6768aaf66a860358120df3c36cd62"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise_2_helper2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxInt_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",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Def.Words_s.int_to_natN"
      ],
      0,
      "a8929df3900bc9807ab0b46366f4c848"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise_3_helper2",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing",
        "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_BoxInt_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",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Def.Words_s.int_to_natN"
      ],
      0,
      "bf9e2444d7051ca6eb7fc09c05b27454"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise_1_helper3",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_BoxInt_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",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Def.Words_s.int_to_natN"
      ],
      0,
      "66ffcf075edf6d286ff42e5a68522dd8"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise_2_helper3",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo0",
        "proj_equation_Vale.Def.Words_s.Mkfour_lo1",
        "projection_inverse_BoxInt_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",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Def.Words_s.int_to_natN"
      ],
      0,
      "b3ed05718e206b8af28f251610159ddd"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise_3_helper3",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing",
        "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_BoxInt_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",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Def.Words_s.int_to_natN"
      ],
      0,
      "3984117246913260f2c1708dff17d78e"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise_1",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "8f8d80c847005288c0c02d84c2c9ee9c"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise_2",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "54ccbafa38c080d85d4621c65ba4b24b"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise_3",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "d8943e797e82c14773f90fe673fccb72"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise_4",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_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",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "typing_Vale.Def.Words_s.int_to_natN"
      ],
      0,
      "3591164a95e492784b183a0615657f78"
    ],
    [
      "Vale.AES.GCTR.nat32_xor_bytewise",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seq_to_four_LE",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat8",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat8", "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_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_FStar.Seq.Properties.slice_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan",
        "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_hi3",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice"
      ],
      0,
      "535660b131703647960b6451354669df"
    ],
    [
      "Vale.AES.GCTR.lemma_slices_le_quad32_to_bytes",
      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",
        "Vale.AES.GCTR_interpretation_Tm_arrow_4217d864395e427d3d50043a7013186f",
        "Vale.AES.GCTR_interpretation_Tm_arrow_d99575c656699ec1bf0db12d4bfb9bae",
        "Vale.Def.Words.Four_s_interpretation_Tm_arrow_3411db9d06d17e1f56929dd49c5039c7",
        "constructor_distinct_Tm_unit", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Four_s.four_select",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seq_to_four_LE",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "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_FStar.Seq.Base.index",
        "function_token_typing_Vale.Def.Types_s.le_quad32_to_bytes",
        "function_token_typing_Vale.Def.Words.Four_s.nat_to_four",
        "function_token_typing_Vale.Def.Words.Seq_s.seq_four_to_seq_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_4f03474956a6a2311e7d7bb19e902da5",
        "interpretation_Tm_abs_52c1d4d343bbe70c2e38480b65b4fb43",
        "interpretation_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac",
        "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_init_len",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.UInt.pow2_values",
        "lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8",
        "primitive_Prims.op_Addition", "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_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
        "refinement_interpretation_Tm_refine_b75956299d71331caf39bdc95ee7a81c",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f21dd5802eb4c999bcae09802023d5fd",
        "token_correspondence_Vale.Def.Words.Four_s.nat_to_four",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.init",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca",
        "typing_Tm_abs_4f03474956a6a2311e7d7bb19e902da5",
        "typing_Tm_abs_d14cec5377e4a5ae1673ba8d887b6dac",
        "typing_Vale.Def.Types_s.le_quad32_to_bytes",
        "typing_Vale.Def.Words.Four_s.four_to_nat",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
        "typing_Vale.Def.Words.Seq_s.seq_to_four_LE",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1"
      ],
      0,
      "13aad8687274605d82d4e9fb547a4ba8"
    ],
    [
      "Vale.AES.GCTR.quad32_xor_bytewise",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Types_s.quad32_xor_def",
        "equation_Vale.Def.Words.Seq_s.seq_to_four_LE",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Types_s.quad32_xor",
        "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_eq_refl",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_length",
        "lemma_FStar.Seq.Properties.slice_slice",
        "primitive_Prims.op_Addition", "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",
        "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",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_49442ef358733fc3ea5275d290f1a90a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_Vale.Def.Types_s.quad32_xor_def",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
        "typing_Vale.Def.Types_s.quad32_xor", "unit_inversion"
      ],
      0,
      "e27fb1bcb1740819f8d3647d7df0db96"
    ],
    [
      "Vale.AES.GCTR.slice_pad_to_128_bits",
      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_slice",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_length",
        "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",
        "refinement_interpretation_Tm_refine_ee7b6e756c39827ea7822b443c038504",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length"
      ],
      0,
      "53f18a02e036ee25d904c91c0b4057c9"
    ],
    [
      "Vale.AES.GCTR.step2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Vale.AES.AES_s.aes_key_LE",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_block",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Def.Types_s.quad32",
        "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.int",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
        "int_typing", "lemma_FStar.Seq.Base.hasEq_lemma",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_ee7b6e756c39827ea7822b443c038504",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length"
      ],
      0,
      "d4468cf8deb1998746d2be9398ed1078"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_to_full_advanced",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "eq2-interp",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "equation_Vale.Def.Words_s.nat8",
        "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
        "int_typing", "l_and-interp", "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "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_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
      ],
      0,
      "67a19de8dd20504683acf2d0b618c6e8"
    ],
    [
      "Vale.AES.GCTR.gctr_partial_to_full_advanced",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Base.op_At_Bar",
        "equation_FStar.Seq.Properties.split", "equation_Prims.nat",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_LE_def",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_block",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.Def.Types_s.quad32",
        "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_Vale.AES.GCTR_s.gctr_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",
        "lemma_FStar.Seq.Base.lemma_create_len",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_FStar.Seq.Properties.slice_slice",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "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_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_507ed4c55777344d5e25694fb1d7ecf2",
        "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_e1bea99dc78d1ca62997794b26d8be1c",
        "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_LE_def",
        "typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice",
        "typing_Vale.AES.AES_s.aes_encrypt_LE",
        "typing_Vale.AES.GCTR_s.inc32",
        "typing_Vale.Def.Types_s.le_quad32_to_bytes",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "typing_Vale.Def.Types_s.quad32_xor",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32"
      ],
      0,
      "0260db60d9ad8005774d595c337bdf97"
    ],
    [
      "Vale.AES.GCTR.gctr_encrypt_one_block",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "f662e52f27addaecbbcd48588cc13799"
    ],
    [
      "Vale.AES.GCTR.gctr_encrypt_one_block",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.Seq.Properties.cons",
        "equation_FStar.Seq.Properties.head",
        "equation_FStar.Seq.Properties.tail", "equation_Prims.nat",
        "equation_Vale.AES.AES_s.aes_key_LE",
        "equation_Vale.AES.GCTR.aes_encrypt_BE",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_LE_def",
        "equation_Vale.AES.GCTR_s.gctr_encrypt_block",
        "equation_Vale.AES.GCTR_s.gctr_plain_internal_LE",
        "equation_Vale.AES.GCTR_s.inc32", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "equation_with_fuel_Vale.AES.GCTR_s.gctr_encrypt_recursive.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.AES.GCTR_s.gctr_encrypt_LE",
        "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_index_create",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "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_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "token_correspondence_Vale.AES.GCTR_s.gctr_encrypt_LE_def",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0"
      ],
      0,
      "6f21952df74b3e619f694c830a98a042"
    ],
    [
      "Vale.AES.GCTR.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_FStar.Seq.Base.op_At_Bar", "equation_Prims.l_and",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
        "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,
      "752eed810f315c2c2abaaf28d0f7cb57"
    ],
    [
      "Vale.AES.GCTR.gctr_bytes_helper",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "eq2-interp", "equation_Prims.nat", "equation_Prims.squash",
        "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",
        "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "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_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.Seq.Base.append"
      ],
      0,
      "147db2e1b9405d2df959e05e47ed346f"
    ],
    [
      "Vale.AES.GCTR.gctr_bytes_helper",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.min",
        "equation_Prims.nat", "equation_Vale.AES.GCTR.aes_encrypt_BE",
        "equation_Vale.AES.GCTR.gctr_partial_def",
        "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_s.nat32", "equation_Vale.Def.Words_s.nat8",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.AES.GCTR.gctr_partial",
        "function_token_typing_Vale.AES.GCTR.gctr_partial_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_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_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_Equality",
        "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",
        "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",
        "refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "token_correspondence_Vale.AES.GCTR.gctr_partial",
        "token_correspondence_Vale.AES.GCTR.gctr_partial_def",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.op_At_Bar",
        "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
      ],
      0,
      "794c7d128f086511387acd548d3cbfdb"
    ]
  ]
]