[
  "\u0004cä¥]ã\u001e•¸\u0015GX\u001aöIŒ",
  [
    [
      "Vale.AES.X64.AESopt2.scratch_b_blocks",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "0d39cd83321664992f49f45b55ad372d"
    ],
    [
      "Vale.AES.X64.AESopt2.va_lemma_MulAdd_step",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "equation_Prims.nat",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "primitive_Prims.op_Equality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Vale.X64.CPU_Features_s.avx_enabled"
      ],
      0,
      "a9d5fa76649c3325c0e5a1d21c193bfb"
    ],
    [
      "Vale.AES.X64.AESopt2.va_wp_MulAdd_step",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "402a64a6d451a6edf23849e0fd1269c8"
    ],
    [
      "Vale.AES.X64.AESopt2.va_quick_MulAdd_step",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "e2e64010afa24ed39b5a05b8f0ff9320"
    ],
    [
      "Vale.AES.X64.AESopt2.va_lemma_ReduceLast",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "36f246d1386fb5a9d4350e2887c8e6d2"
    ],
    [
      "Vale.AES.X64.AESopt2.va_wp_ReduceLast",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "959c802892ed676fda1bd0b29324bcf6"
    ],
    [
      "Vale.AES.X64.AESopt2.va_quick_ReduceLast",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "1ba5dec2e004179c82cb3efa3cc87f4b"
    ],
    [
      "Vale.AES.X64.AESopt2.va_quick_GhashUnroll_n",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "42be9f3e58910c08ae6f61cc87038b06"
    ],
    [
      "Vale.AES.X64.AESopt2.va_quick_Ghash_register",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "43fbd85a523540c92c0cbbbbdbfe8571"
    ],
    [
      "Vale.AES.X64.AESopt2.va_quick_Ghash_buffer",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "8fdfeb845580a1f9f8ee41f5af41d913"
    ],
    [
      "Vale.AES.X64.AESopt2.va_lemma_GhashUnroll6x",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "aec84eb4a016a137d06ccd192f458485"
    ],
    [
      "Vale.AES.X64.AESopt2.va_wp_GhashUnroll6x",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "9f6429b2fa4c569e38688b6856613a91"
    ],
    [
      "Vale.AES.X64.AESopt2.va_quick_GhashUnroll6x",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "ace8dd6a1c7b11f7e31c1b03c81ffc31"
    ]
  ]
]