[
  "�\"�u�^�\u000b�\\0\u001fl�\u0003&",
  [
    [
      "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,
      "102df3ae00b3a20a927338aaa9672a49"
    ],
    [
      "Vale.AES.X64.AES256.va_wp_KeyExpansion256Stdcall",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "4dc0b442f2ff5109ea04d817bbf74794"
    ],
    [
      "Vale.AES.X64.AES256.va_quick_KeyExpansion256Stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "690915a491874a95a10641721dee6c46"
    ],
    [
      "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",
        "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_6e43015ff945324816792ff05c5cdc82"
      ],
      0,
      "60521813f413fd760612e13497e57b99"
    ],
    [
      "Vale.AES.X64.AES256.va_wp_AES256EncryptBlock",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "9004a35f9000846dff574647650af1ad"
    ],
    [
      "Vale.AES.X64.AES256.va_quick_AES256EncryptBlock",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "fd28974e233729fe783ba3d0757f8c9d"
    ],
    [
      "Vale.AES.X64.AES256.va_lemma_AES256EncryptBlockStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion", "eq2-interp",
        "equality_tok_Vale.X64.Machine_s.Secret@tok",
        "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",
        "equation_Vale.X64.Decls.validDstAddrs128",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Memory.get_vale_heap",
        "fuel_guarded_inversion_Vale.Def.Words_s.four",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0643373093c4f5346cab366112399d5a",
        "refinement_interpretation_Tm_refine_4d38686bf695f79f110ce5aef057279f"
      ],
      0,
      "df4efedec70a5ba94d9a5a48ce911c6f"
    ],
    [
      "Vale.AES.X64.AES256.va_wp_AES256EncryptBlockStdcall",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "a5e1ee119945ee2f6102974c36708332"
    ],
    [
      "Vale.AES.X64.AES256.va_quick_AES256EncryptBlockStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "31afe01c0619277b872542fad2fbbb71"
    ]
  ]
]