[
  "\tj&F�ދ�\u0016����(\bf",
  [
    [
      "Vale.AES.X64.GF128_Init.va_req_Keyhash_init",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "unit_typing"
      ],
      0,
      "86177a58052506c58e11fae5f6f4f40d"
    ],
    [
      "Vale.AES.X64.GF128_Init.va_ens_Keyhash_init",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "equation_Vale.AES.X64.GF128_Init.va_req_Keyhash_init",
        "equation_Vale.X64.Decls.va_state_eq",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
        "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
        "unit_typing"
      ],
      0,
      "6d082d892d0450474e4c4c16d9b032f5"
    ],
    [
      "Vale.AES.X64.GF128_Init.va_lemma_Keyhash_init",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "equation_Vale.X64.Decls.va_require_total",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "refinement_interpretation_Tm_refine_a5c7b042be3094d09e1325f52034d356"
      ],
      0,
      "7f6a5562935b88444c436392ae2036ab"
    ],
    [
      "Vale.AES.X64.GF128_Init.va_wp_Keyhash_init",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "55bf90796ffa855f91d795c086a4acb6"
    ],
    [
      "Vale.AES.X64.GF128_Init.va_quick_Keyhash_init",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "7d8aa44207ab0f93e507a53d01009bee"
    ]
  ]
]