[
  "®»èŒ.ùú§Æ×\u001bU—ƒZ‚",
  [
    [
      "Vale.AES.X64.GHash.get_last_slice_workaround",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
        "equation_Prims.nat", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
        "kinding_Vale.Def.Words_s.four@tok",
        "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_AmpAmp",
        "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_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647"
      ],
      0,
      "5c23f8c0ab3c9cd19125e3407dcfe7a8"
    ],
    [
      "Vale.AES.X64.GHash.va_quick_Compute_ghash_incremental_register",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "ae6af6f6702560e8e3e88b45f38e1007"
    ]
  ]
]