[
  "ÿ)Nyñö¬@rW/*¶3^\u000f",
  [
    [
      "Vale.AES.GHash.fun_seq_quad32_LE_poly128",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
        "int_inversion", "lemma_Vale.Math.Poly2.Bits.lemma_of_quad32_degree",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303"
      ],
      0,
      "93f0262f3024e6f55bd908fb862d603d"
    ],
    [
      "Vale.AES.GHash.ghash_poly",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Prims.LexTop@tok",
        "int_typing", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxInt_proj_0", "well-founded-ordering-on-nat"
      ],
      0,
      "2a3a0ed367c613a40c50d64caa98b71b"
    ],
    [
      "Vale.AES.GHash.g_power",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals", "int_inversion",
        "int_typing", "primitive_Prims.op_Equality",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "4413a159e4b0c5e85ff9353702d464af"
    ],
    [
      "Vale.AES.GHash.lemma_g_power_1",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "equation_with_fuel_Vale.AES.GHash.g_power.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "734a9f1491816b48583651bf31d25f4e"
    ],
    [
      "Vale.AES.GHash.lemma_g_power_n",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.pos",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "3bc8efe1204244148c16f4c34f237eae"
    ],
    [
      "Vale.AES.GHash.lemma_g_power_n",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.g_power.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Vale.AES.GHash.g_power.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "66310df3cd72b11281bef42af4b41b6c"
    ],
    [
      "Vale.AES.GHash.lemma_gf128_power",
      1,
      1,
      0,
      [
        "@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
        "@query", "equation_Vale.AES.GHash.gf128_power",
        "equation_Vale.AES.GHash.shift_gf128_key_1"
      ],
      0,
      "a5f24844819ff1a976f1cec8b7b80c05"
    ],
    [
      "Vale.AES.GHash.hkeys_reqs_priv",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
        "equation_Vale.Def.Types_s.quad32",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "typing_Vale.Def.Types_s.quad32"
      ],
      0,
      "c73c31a8e336ca8601b774fe3a00bfaf"
    ],
    [
      "Vale.AES.GHash.ghash_poly_unroll",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_ae567c2fb75be05905677af440075565_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "6301c05eb7f6421e230aedde9bd08264"
    ],
    [
      "Vale.AES.GHash.lemma_hkeys_reqs_pub_priv",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
        "@fuel_correspondence_Vale.AES.OptPublic.g_power.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.g_power.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.OptPublic.g_power.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "b2t_def", "bool_inversion", "bool_typing", "eq2-interp",
        "equation_Prims.nat", "equation_Vale.AES.GHash.gf128_power",
        "equation_Vale.AES.GHash.hkeys_reqs_priv",
        "equation_Vale.AES.GHash.shift_gf128_key_1",
        "equation_Vale.AES.OptPublic.gf128_power",
        "equation_Vale.AES.OptPublic.hkeys_reqs_pub",
        "equation_Vale.AES.OptPublic.shift_gf128_key_1",
        "equation_with_fuel_Vale.AES.GHash.g_power.fuel_instrumented",
        "equation_with_fuel_Vale.AES.OptPublic.g_power.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "l_and-interp", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_Vale.Math.Poly2.Bits_s.of_quad32"
      ],
      0,
      "e1e7930a6db3e3746db5a197c4463bc9"
    ],
    [
      "Vale.AES.GHash.ghash_unroll",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_ae567c2fb75be05905677af440075565_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "90b9168d53dbc7ab841b9658f473b179"
    ],
    [
      "Vale.AES.GHash.ghash_unroll_back",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_ae567c2fb75be05905677af440075565_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "e65242d1879f5dabc4eeaeace253a2bd"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_unroll_back_forward_rec",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
        "equation_Prims.squash", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_9962406f6ed02d6f297636707e1f9a85"
      ],
      0,
      "f16b97ba28546abff3d61421b889e55f"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_unroll_back_forward_rec",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
        "@fuel_correspondence_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.AES.GHash_interpretation_Tm_arrow_15ceef7ed9aea3b9eeb1e60e5343be5b",
        "b2t_def", "binder_x_4926595fe3e8db262b015229c320f9d3_2",
        "binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_0",
        "binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
        "binder_x_ae567c2fb75be05905677af440075565_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals", "equation_Prims.squash",
        "equation_Vale.AES.GHash.poly128",
        "equation_with_fuel_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
        "equation_with_fuel_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_01bf4ea4232daa099d3c1a9e6ea80dd0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f54be9bebc70c1c037e0ec20437e5c81",
        "typing_Vale.AES.GHash.gf128_power",
        "typing_Vale.AES.GHash.ghash_unroll",
        "typing_Vale.AES.GHash.ghash_unroll_back",
        "typing_Vale.Math.Poly2_s.mul", "well-founded-ordering-on-nat"
      ],
      0,
      "ba531d160a05b52f729672d4f22cf09b"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_unroll_back_forward",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "3de8caefe0171e240f282f0f70d3717f"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_unroll_back_forward",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
        "@fuel_correspondence_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat",
        "equation_with_fuel_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
        "equation_with_fuel_Vale.AES.GHash.ghash_unroll_back.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Vale.AES.GHash.ghash_unroll",
        "typing_Vale.AES.GHash.ghash_unroll_back"
      ],
      0,
      "af41fe3aab06bc2886db666304e5717a"
    ],
    [
      "Vale.AES.GHash.lemma_gf128_mul_rev_mod_rev",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Vale.AES.GF128.gf128_mul_rev",
        "equation_Vale.AES.GF128.mod_rev",
        "equation_Vale.AES.GF128.shift_key_1",
        "equation_Vale.AES.GF128_s.gf128_modulus",
        "equation_Vale.AES.GF128_s.gf128_modulus_low_terms",
        "equation_Vale.AES.GF128_s.gf128_mul",
        "equation_Vale.AES.GHash.shift_gf128_key_1",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
        "int_typing",
        "interpretation_Tm_abs_91a45626d634360d0cb72d9b8d62e58c",
        "lemma_Vale.Math.Poly2.Lemmas.lemma_mask_degree",
        "lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
        "lemma_Vale.Math.Poly2.lemma_add_degree",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303",
        "refinement_interpretation_Tm_refine_fe6ca960360a1d9d67a3dd4cf32a29b0",
        "typing_Tm_abs_91a45626d634360d0cb72d9b8d62e58c",
        "typing_Vale.AES.GF128_s.gf128_modulus",
        "typing_Vale.AES.GHash.shift_gf128_key_1",
        "typing_Vale.Math.Poly2.mask", "typing_Vale.Math.Poly2_s.monomial",
        "typing_Vale.Math.Poly2_s.of_fun",
        "typing_Vale.Math.Poly2_s.reverse", "typing_Vale.Math.Poly2_s.shift",
        "typing_Vale.Math.Poly2_s.zero"
      ],
      0,
      "6bb601b27a9c1542c399b7b8694f15fe"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_poly_degree",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GHash.ghash_poly.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.ghash_poly.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.AES.GHash_interpretation_Tm_arrow_15ceef7ed9aea3b9eeb1e60e5343be5b",
        "binder_x_4926595fe3e8db262b015229c320f9d3_2",
        "binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_0",
        "binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
        "binder_x_ae567c2fb75be05905677af440075565_3",
        "binder_x_ae567c2fb75be05905677af440075565_4",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "equation_Vale.AES.GF128.gf128_mul_rev",
        "equation_Vale.AES.GHash.poly128",
        "equation_with_fuel_Vale.AES.GHash.ghash_poly.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
        "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f54be9bebc70c1c037e0ec20437e5c81",
        "token_correspondence_Vale.AES.GHash.ghash_poly.fuel_instrumented",
        "typing_Vale.AES.GF128_s.gf128_mul",
        "typing_Vale.AES.GHash.ghash_poly", "typing_Vale.Math.Poly2_s.add",
        "typing_Vale.Math.Poly2_s.reverse", "well-founded-ordering-on-nat"
      ],
      0,
      "bb66c24a7f45baf6bebf36a3ce823bcb"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_poly_unroll_n",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_e313cad38295948172e35d15f4ce8e0e"
      ],
      0,
      "54550c47e92203ed7944e40debf3b4ce"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_poly_unroll_n",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
        "@fuel_correspondence_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.g_power.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_4926595fe3e8db262b015229c320f9d3_2",
        "binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_0",
        "binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
        "binder_x_ae567c2fb75be05905677af440075565_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "equation_with_fuel_Vale.AES.GHash.g_power.fuel_instrumented",
        "equation_with_fuel_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "well-founded-ordering-on-nat"
      ],
      0,
      "c878fae4bbbc2174b6ee44194398a4c2"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_poly_unroll",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
        "@fuel_correspondence_Vale.AES.GHash.ghash_poly.fuel_instrumented",
        "@fuel_correspondence_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.ghash_poly.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_4926595fe3e8db262b015229c320f9d3_2",
        "binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_0",
        "binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
        "binder_x_ae567c2fb75be05905677af440075565_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "equation_Vale.AES.GF128.op_Star_Tilde",
        "equation_with_fuel_Vale.AES.GHash.g_power.fuel_instrumented",
        "equation_with_fuel_Vale.AES.GHash.ghash_poly.fuel_instrumented",
        "equation_with_fuel_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "primitive_Prims.op_Equality",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "token_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
        "typing_Vale.AES.GHash.g_power", "typing_Vale.AES.GHash.ghash_poly",
        "well-founded-ordering-on-nat"
      ],
      0,
      "ba318209e126c6ad7f8acd2ce6dfe651"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_unroll_poly_unroll",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
        "@fuel_correspondence_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
        "@fuel_correspondence_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Vale.AES.GHash_interpretation_Tm_arrow_15ceef7ed9aea3b9eeb1e60e5343be5b",
        "binder_x_4926595fe3e8db262b015229c320f9d3_2",
        "binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_0",
        "binder_x_502cb01ef05aa03f246ba4bf1abd0f3f_1",
        "binder_x_ae567c2fb75be05905677af440075565_3",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_4",
        "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5", "equation_Prims.nat",
        "equation_Prims.op_Equals_Equals_Equals",
        "equation_Vale.AES.GF128.gf128_mul_rev",
        "equation_Vale.AES.GF128.op_Star_Tilde",
        "equation_Vale.AES.GHash.gf128_power",
        "equation_Vale.AES.GHash.poly128",
        "equation_with_fuel_Vale.AES.GHash.g_power.fuel_instrumented",
        "equation_with_fuel_Vale.AES.GHash.ghash_poly_unroll.fuel_instrumented",
        "equation_with_fuel_Vale.AES.GHash.ghash_unroll.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Math.Poly2.Lemmas.lemma_zero_degree",
        "int_inversion", "int_typing",
        "lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
        "lemma_Vale.Math.Poly2.lemma_add_degree",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_6c3579831eb81025494abc2bedea1303",
        "refinement_interpretation_Tm_refine_f54be9bebc70c1c037e0ec20437e5c81",
        "token_correspondence_Vale.AES.GHash.g_power.fuel_instrumented",
        "typing_Vale.AES.GF128_s.gf128_mul",
        "typing_Vale.Math.Poly2_s.reverse", "well-founded-ordering-on-nat"
      ],
      0,
      "00d9db0feb26f2ec505d6c540749019c"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_poly_of_unroll",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "d14083a0b73240accecd804b8b66989e"
    ],
    [
      "Vale.AES.GHash.lemma_add_manip",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "f34a09a3a0818de2b704541a2ae403a2"
    ],
    [
      "Vale.AES.GHash.ghash_incremental_def",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_2",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Lib.Seqs_s.all_but_last",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "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",
        "typing_FStar.Seq.Base.length", "well-founded-ordering-on-nat"
      ],
      0,
      "fc83bf36b2d354421de58972509d9d3d"
    ],
    [
      "Vale.AES.GHash.ghash_incremental_reveal",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "1c38e00cc3be3da85ad08ad1a888ad6d"
    ],
    [
      "Vale.AES.GHash.lemma_reverse_bytes_quad32_xor",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
        "Vale.Lib.Seqs_s_interpretation_Tm_arrow_5ead088aae36f5466dc4f492316985f2",
        "b2t_def", "bool_inversion", "bool_typing",
        "data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Vale.Def.Types_s.be_bytes_to_nat32",
        "equation_Vale.Def.Types_s.nat32_to_be_bytes",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Types_s.quad32_xor_def",
        "equation_Vale.Def.Types_s.reverse_bytes_nat32_def",
        "equation_Vale.Def.Words.Four_s.four_reverse",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seq_to_four_BE",
        "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.reverse_seq",
        "equation_Vale.Math.Bits.lemmas_i2b_all",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Vale.Def.Types_s.quad32_xor",
        "function_token_typing_Vale.Def.Types_s.reverse_bytes_nat32",
        "function_token_typing_Vale.Def.Words_s.nat8",
        "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c",
        "l_quant_interp_48240b4f3858918eae686ff2a62a9fe7",
        "l_quant_interp_ab92dcdc665fc6e1201234d45389b203",
        "lemma_FStar.Seq.Base.init_index_",
        "lemma_FStar.Seq.Base.lemma_init_len",
        "lemma_FStar.UInt.pow2_values",
        "lemma_Vale.Def.Words.Seq.four_to_nat_to_four_8",
        "lemma_Vale.Def.Words.Seq.nat_to_four_to_nat",
        "lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree",
        "primitive_Prims.op_AmpAmp", "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_BoxBitVec32_proj_0",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Def.Words_s.Mkfour_a",
        "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_0c91e66c97ed3054dc88c856ecfaebc1",
        "refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e",
        "refinement_interpretation_Tm_refine_30c926ebf383bedbae82319bb48dcf51",
        "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
        "refinement_interpretation_Tm_refine_637bf9344435626707effe179cd350a8",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_c6a5ae056cb5a72f4660066bbd48d8bd",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "refinement_interpretation_Tm_refine_fae547c0c57b476075b6de4468df2cfa",
        "token_correspondence_Vale.Def.Types_s.quad32_xor_def",
        "token_correspondence_Vale.Def.Types_s.reverse_bytes_nat32_def",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
        "typing_Prims.pow2",
        "typing_Tm_abs_e33894a065c7d8cf9373282d9aa6a27c",
        "typing_Vale.Def.Types_s.ixor",
        "typing_Vale.Def.Types_s.nat32_to_be_bytes",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
        "typing_Vale.Def.Words.Seq_s.seq_to_four_BE",
        "typing_Vale.Def.Words_s.int_to_natN",
        "typing_Vale.Math.Bits.add_hide", "typing_Vale.Math.Bits.mul_hide",
        "typing_Vale.Math.Poly2.Bits.of_nat32",
        "typing_Vale.Math.Poly2_s.degree"
      ],
      0,
      "22d9c3560253f87b52f550a927615154"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_incremental_poly_rec",
      1,
      1,
      0,
      [
        "@query", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "eec57bb2f85e13c7ff17c45b5af91c19"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_incremental_poly_rec",
      2,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
        "@fuel_correspondence_Vale.AES.GHash.ghash_poly.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.ghash_poly.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "binder_x_4926595fe3e8db262b015229c320f9d3_3",
        "binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_2",
        "binder_x_e97427d583e1f4d42a96b4bdd8dae147_0",
        "binder_x_e97427d583e1f4d42a96b4bdd8dae147_1",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.last", "equation_Prims.nat",
        "equation_Vale.AES.GF128.gf128_mul_rev",
        "equation_Vale.AES.GF128.op_Star_Tilde",
        "equation_Vale.AES.GF128_s.gf128_of_quad32",
        "equation_Vale.AES.GF128_s.gf128_to_quad32",
        "equation_Vale.AES.GHash_s.gf128_mul_LE",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Lib.Seqs_s.all_but_last",
        "equation_with_fuel_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
        "equation_with_fuel_Vale.AES.GHash.ghash_poly.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",
        "l_quant_interp_9d28f2c215748aabc91cf2d5039b0560",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.Arch.Types.lemma_reverse_bytes_quad32",
        "lemma_Vale.Math.Poly2.Lemmas.lemma_reverse_degree",
        "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_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "typing_FStar.Seq.Base.length", "typing_Vale.AES.GF128_s.gf128_mul",
        "typing_Vale.AES.GF128_s.gf128_of_quad32",
        "typing_Vale.AES.GF128_s.gf128_to_quad32",
        "typing_Vale.Def.Types_s.quad32_xor",
        "typing_Vale.Def.Types_s.reverse_bytes_quad32",
        "typing_Vale.Math.Poly2.Bits_s.of_quad32",
        "typing_Vale.Math.Poly2_s.reverse", "well-founded-ordering-on-nat"
      ],
      0,
      "f65439e239b6500dcce225a4af5cc192"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_incremental_poly",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Vale.AES.GHash.fun_seq_quad32_LE_poly128",
        "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.GHash.ghash_incremental",
        "function_token_typing_Vale.AES.GHash.ghash_incremental_def",
        "int_inversion",
        "interpretation_Tm_abs_2a4e5f30c6fdc83783b57e5a74d18144",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "token_correspondence_Vale.AES.GHash.fun_seq_quad32_LE_poly128"
      ],
      0,
      "809c53861997a55fa9897bcbbf317f45"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_incremental_def_0",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_with_fuel_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__",
        "primitive_Prims.op_Equality"
      ],
      0,
      "1e0f7c700d2542366ccef1b01888f6e7"
    ],
    [
      "Vale.AES.GHash.ghash_incremental_to_ghash",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "bf44e26fe3f49487df23b2274f799422"
    ],
    [
      "Vale.AES.GHash.ghash_incremental_to_ghash",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
        "primitive_Prims.op_GreaterThan",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
      ],
      0,
      "3b5ebfec20726d1957af804611eae631"
    ],
    [
      "Vale.AES.GHash.ghash_incremental_to_ghash",
      3,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
        "@fuel_correspondence_Vale.AES.GHash_s.ghash_LE_def.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash_s.ghash_LE_def.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_e4836109f73687024ac3edd113084865",
        "binder_x_611f4d9b9b7ca657fff97fd0b29bf02c_1",
        "binder_x_e97427d583e1f4d42a96b4bdd8dae147_0",
        "data_typing_intro_Vale.Def.Words_s.Mkfour@tok",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "equation_Vale.AES.GHash_s.ghash_plain_LE",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
        "equation_Vale.Lib.Seqs_s.all_but_last",
        "equation_with_fuel_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
        "equation_with_fuel_Vale.AES.GHash_s.ghash_LE_def.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.AES.GHash.ghash_incremental",
        "function_token_typing_Vale.AES.GHash_s.ghash_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_len_slice",
        "lemma_FStar.Seq.Properties.slice_is_empty",
        "lemma_Vale.AES.GHash.lemma_ghash_incremental_def_0",
        "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_3cde0f73125500a52bff30114a1a1137",
        "refinement_interpretation_Tm_refine_3e04674625ba1e90ddf6da6977508e33",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
        "refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "token_correspondence_Vale.AES.GHash.ghash_incremental_def",
        "token_correspondence_Vale.AES.GHash_s.ghash_LE_def",
        "typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
        "typing_Vale.Lib.Seqs_s.all_but_last", "typing_tok_Prims.LexTop@tok",
        "well-founded-ordering-on-nat"
      ],
      0,
      "ed33806873089216cde5c7e552c68fce"
    ],
    [
      "Vale.AES.GHash.lemma_hash_append",
      1,
      1,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
        "@fuel_irrelevance_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
        "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_e4836109f73687024ac3edd113084865",
        "binder_x_cee79fb2a0b31329a2e2b29d477b66be_2",
        "binder_x_cee79fb2a0b31329a2e2b29d477b66be_3",
        "binder_x_e97427d583e1f4d42a96b4bdd8dae147_0",
        "binder_x_e97427d583e1f4d42a96b4bdd8dae147_1",
        "equality_tok_Prims.LexTop@tok",
        "equation_FStar.Seq.Properties.last", "equation_Prims.nat",
        "equation_Vale.AES.GHash_s.ghash_plain_LE",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.Lib.Seqs_s.all_but_last",
        "equation_with_fuel_Vale.AES.GHash.ghash_incremental_def.fuel_instrumented",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.AES.GHash.ghash_incremental",
        "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_app2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "lemma_FStar.Seq.Base.lemma_len_slice",
        "lemma_Vale.AES.GHash.lemma_ghash_incremental_def_0",
        "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_3cde0f73125500a52bff30114a1a1137",
        "refinement_interpretation_Tm_refine_3e04674625ba1e90ddf6da6977508e33",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "token_correspondence_Vale.AES.GHash.ghash_incremental_def",
        "typing_FStar.Seq.Base.length",
        "typing_Vale.AES.GHash.ghash_incremental",
        "typing_Vale.Lib.Seqs_s.all_but_last", "typing_tok_Prims.LexTop@tok",
        "well-founded-ordering-on-nat"
      ],
      0,
      "d7699bbaa06287ac18b2f441e96d25fc"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_incremental0_append",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
        "equation_Vale.AES.GHash.ghash_incremental0",
        "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.Def.Words_s.nat32", "int_inversion",
        "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_index_app1",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar"
      ],
      0,
      "81bdae233624dafdce7ebbd4ee2db7fe"
    ],
    [
      "Vale.AES.GHash.lemma_hash_append2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
        "equation_Vale.AES.GHash.ghash_incremental0",
        "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.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_eq_elim",
        "lemma_FStar.Seq.Base.lemma_eq_intro",
        "lemma_FStar.Seq.Base.lemma_index_app2",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar"
      ],
      0,
      "3509d7f8d55f3581f78d74753ae29824"
    ],
    [
      "Vale.AES.GHash.lemma_hash_append3",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Prims.squash",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat32",
        "kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
        "lemma_FStar.Seq.Base.lemma_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_GreaterThan",
        "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",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
        "typing_Vale.Def.Types_s.quad32"
      ],
      0,
      "0b71b84cb59935d8a9daff54108bd4a3"
    ],
    [
      "Vale.AES.GHash.lemma_hash_append3",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Vale.AES.GHash.ghash_incremental0",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "int_typing", "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_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_len_append",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThan", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
        "unit_inversion", "unit_typing"
      ],
      0,
      "347a93b320aa73fe1eb0afade7d8b846"
    ],
    [
      "Vale.AES.GHash.ghash_incremental_bytes_pure_no_extra",
      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_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "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.length"
      ],
      0,
      "8c9c8f725fb5544481c09724820ec611"
    ],
    [
      "Vale.AES.GHash.ghash_incremental_bytes_pure_no_extra",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "bool_typing", "equation_Prims.nat",
        "equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "equation_Vale.AES.GHash.ghash_incremental0",
        "equation_Vale.Def.Types_s.quad32",
        "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.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_AmpAmp",
        "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1"
      ],
      0,
      "328598c780fb646a21c634b42c560ec0"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "equation_Prims.nat", "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_Prims.__cache_version_number__",
        "int_inversion", "l_and-interp",
        "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
        "typing_Vale.Def.Types_s.le_quad32_to_bytes"
      ],
      0,
      "6f9c518e45bfbda623948f90121508bd"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
        "equation_FStar.Seq.Base.op_At_Bar",
        "equation_FStar.Seq.Properties.split", "equation_Prims.nat",
        "equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
        "equation_Vale.AES.GCTR_s.pad_to_128_bits",
        "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_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_index_slice",
        "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_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_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_9490cfb1c0d2cc8b6f2817cf9207cbd0",
        "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
        "typing_FStar.Seq.Base.slice",
        "typing_Vale.AES.GCTR_s.pad_to_128_bits",
        "typing_Vale.Def.Types_s.le_quad32_to_bytes"
      ],
      0,
      "5cb0e2edae271a194e58d68d40ae3a09"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper_alt",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
        "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.Def.Words_s.nat32", "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_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",
        "refinement_interpretation_Tm_refine_b31e3a3ba71ee334e7dd15a53b9eadcc",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_Vale.Def.Types_s.le_quad32_to_bytes"
      ],
      0,
      "5dd5def6ed7ef2d0fcd5718923c11daf"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_incremental_bytes_extra_helper_alt",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
        "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.Def.Words_s.nat32", "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_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_create",
        "lemma_FStar.Seq.Base.lemma_index_slice",
        "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_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_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
        "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "e2b21182f00789d9f732d6eac9a6d4f2"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_registers",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.nat",
        "equation_Prims.squash", "int_inversion", "l_and-interp",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "7af7c15b92dfb77c5d9689ad06ae17c4"
    ],
    [
      "Vale.AES.GHash.lemma_ghash_registers",
      2,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
        "equation_Vale.AES.GHash.ghash_incremental0",
        "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_create_len",
        "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_create",
        "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_GreaterThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1a5730b11931d46761662d21375532a0",
        "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
        "refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
        "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
        "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,
      "3be78b50d9143cd9b24d33bcd7b8ec63"
    ]
  ]
]