[
  "��!�\u0012\u0011�RљQ\n��l�",
  [
    [
      "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,
      "7106fb883d3551a12247cfddb0b7f4e3"
    ],
    [
      "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,
      "c6f6ec112c4ea864f56f096ba4879d9b"
    ],
    [
      "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,
      "93e49bac96bfcab219e95d0e233c9ef2"
    ],
    [
      "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,
      "0f2870e457705f57033167d40dbc343a"
    ],
    [
      "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",
        "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,
      "d97da2d04fb70933849491f6b27f3c18"
    ],
    [
      "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",
        "equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
        "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,
      "83549b60d169982734408c4c6f0445fe"
    ],
    [
      "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,
      "3c826e20464edc707b94a23fd5cab56c"
    ],
    [
      "Vale.AES.GHash.lemma_add_manip",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "b84640ebff7739330d33422fc30c78d1"
    ],
    [
      "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,
      "88b585df4a20a0f166e741762bd30416"
    ],
    [
      "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,
      "0ce630dffd01196ebf9d0d421e464a2c"
    ],
    [
      "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,
      "bb4f1f2d9768f7d8af34623f6332d0b8"
    ],
    [
      "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,
      "239533b0d5b9be0eff0112993461c08a"
    ],
    [
      "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,
      "da85ff8ef4280203756506ed23b9fe41"
    ],
    [
      "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,
      "faf74056c3294ae010f2d8c892a774ca"
    ],
    [
      "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,
      "1bb3e65f97baf3678cf0d14b802317ba"
    ]
  ]
]