[
  "\u0006�\u0015ս��\u0003\">*ϵ)\u00184",
  [
    [
      "Vale.X64.InsAes.va_quick_Pclmulqdq",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "fa17e6c72eea6956683b0696963fc3f9"
    ],
    [
      "Vale.X64.InsAes.va_quick_VPclmulqdq",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "3a6703c75d514c96e84d0df350c51638"
    ],
    [
      "Vale.X64.InsAes.va_quick_AESNI_enc",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "5c39f0650d0db818017addf362431e97"
    ],
    [
      "Vale.X64.InsAes.va_quick_VAESNI_enc",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "c8e5232bbc4d64632ebaf89d4b87720f"
    ],
    [
      "Vale.X64.InsAes.va_quick_AESNI_enc_last",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "e4f1b32caf89dcc0d247c25adfd322ec"
    ],
    [
      "Vale.X64.InsAes.va_quick_VAESNI_enc_last",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "600a9a30b971ccd40b5b19f6a5317b42"
    ],
    [
      "Vale.X64.InsAes.va_lemma_AESNI_keygen_assist",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "c8b64d05a2f9549f50b6e6f1a08e214e"
    ],
    [
      "Vale.X64.InsAes.va_wp_AESNI_keygen_assist",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words_s.nat8",
        "equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
      ],
      0,
      "9b3da3e8b13b1adbc11518ca7bb46820"
    ],
    [
      "Vale.X64.InsAes.va_quick_AESNI_keygen_assist",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "4123046b7bf5eca0f7a67ce4a2b2faa2"
    ]
  ]
]