[
  "8þÉÝ(þ7KhtÔ‹3ú‰d",
  [
    [
      "Vale.AES.X64.AES256.va_lemma_KeyExpansion256Stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
        "equality_tok_Vale.X64.Machine_s.Secret@tok",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Decls.validDstAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_19dcbe503f461f8f8cd69d68660086f5"
      ],
      0,
      "2d824f929b963f5cc6dbfe7804cfef38"
    ],
    [
      "Vale.AES.X64.AES256.va_wp_KeyExpansion256Stdcall",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "c1948d4400c0d1cf53ad9f29a781f1c3"
    ],
    [
      "Vale.AES.X64.AES256.va_quick_KeyExpansion256Stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "0848b6e76499c2ad89ce211a99c4c5cc"
    ],
    [
      "Vale.AES.X64.AES256.va_lemma_AES256EncryptBlock",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.X64.Decls.va_require_total",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0818b6c65d5ada453a3d58953b442cba"
      ],
      0,
      "914cd252932f474ddcf626122dc8f30e"
    ],
    [
      "Vale.AES.X64.AES256.va_wp_AES256EncryptBlock",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "cdc20ca4ce15e0aead35955d336f3222"
    ],
    [
      "Vale.AES.X64.AES256.va_quick_AES256EncryptBlock",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "612c48b3125b88d469b546baa2bacada"
    ],
    [
      "Vale.AES.X64.AES256.va_lemma_AES256EncryptBlockStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.X64.Decls.va_int_range",
        "equation_Vale.X64.Decls.va_require_total",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_4d38686bf695f79f110ce5aef057279f",
        "refinement_interpretation_Tm_refine_a725af384906eab1d4c94068c327bac6"
      ],
      0,
      "2bbdcbc917bd2d9d124aab77a255b548"
    ],
    [
      "Vale.AES.X64.AES256.va_wp_AES256EncryptBlockStdcall",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "b4498ecc09a4b4b31b0f75f9345e06f0"
    ],
    [
      "Vale.AES.X64.AES256.va_quick_AES256EncryptBlockStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "324aa610b2d8282bb854a858410cc6e6"
    ]
  ]
]