[
  "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,
      "72db30c4d4ac57b3cf245e3f48a5130d"
    ],
    [
      "Vale.AES.X64.AES256.va_wp_KeyExpansion256Stdcall",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "cbe8ac30f6a5c77859f3c72da3b201db"
    ],
    [
      "Vale.AES.X64.AES256.va_quick_KeyExpansion256Stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "f4fd4a60a03ee816402fe8b555a3c25d"
    ],
    [
      "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,
      "67223f7af8dd6562dac2e48d532e7eb1"
    ],
    [
      "Vale.AES.X64.AES256.va_wp_AES256EncryptBlock",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "2d0967ca1e7506dfbda46e10df01ff67"
    ],
    [
      "Vale.AES.X64.AES256.va_quick_AES256EncryptBlock",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "fa39387d5e8a28e4cb4096c901b4bb96"
    ],
    [
      "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,
      "1331743aba3f2e175d3915ba40587fd3"
    ],
    [
      "Vale.AES.X64.AES256.va_wp_AES256EncryptBlockStdcall",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "4a3184b0165cd7c84a92c05784c543ca"
    ],
    [
      "Vale.AES.X64.AES256.va_quick_AES256EncryptBlockStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "488210fdeab629d7eb03afc3366e430f"
    ]
  ]
]