[
  "!ĶiAS®L\u0011^[*Ē\u0012\u0005 [",
  [
    [
      "X64.AESstdcall.va_req_AESEncryptBlockStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "unit_typing"
      ],
      0,
      "5f4bb824eae7eb29fd4a1a5f5478986b"
    ],
    [
      "X64.AESstdcall.va_ens_AESEncryptBlockStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "equation_X64.AESstdcall.va_req_AESEncryptBlockStdcall",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "unit_typing"
      ],
      0,
      "ddab859ac0625d90d9db6ac3a4eeb189"
    ],
    [
      "X64.AESstdcall.va_lemma_AESEncryptBlockStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat64",
        "equation_Words_s.natN", "equation_X64.Vale.Decls.validSrcAddrs128",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_fdc852a9618fb4aec61213f1a577bb7c",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_tok_X64.Machine_s.R8@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok"
      ],
      0,
      "1199fa347ba89415fbb4828ee242ae9c"
    ],
    [
      "X64.AESstdcall.va_wp_AESEncryptBlockStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "equation_Prims.nat", "equation_Words_s.nat64",
        "equation_Words_s.natN", "equation_X64.Vale.Decls.va_if",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Words_s.nat64",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad",
        "typing_X64.AES256_Tm_abs_0b85c5cdf81ff9d981d06a423bf17bd6",
        "typing_X64.AES256_Tm_abs_494c4553ff5247f2c81506c212bacc26",
        "typing_X64.AES256_Tm_abs_50ad851d36622cc25536b7edc233d114",
        "typing_X64.AES256_Tm_abs_86b4602d570d0a24c17faa370bd6d79e",
        "typing_X64.Vale.Decls.va_if", "unit_typing"
      ],
      0,
      "714198222723a6f2b57b6d77c1aa17b5"
    ],
    [
      "X64.AESstdcall.va_wpProof_AESEncryptBlockStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "cbb5e80052f8dc8488aa9bb6fd5964f8"
    ],
    [
      "X64.AESstdcall.va_req_aes_EncryptBlockBEStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "unit_typing"
      ],
      0,
      "10959069b37d1c265612782055f94506"
    ],
    [
      "X64.AESstdcall.va_ens_aes_EncryptBlockBEStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.l_and",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "equation_X64.AESstdcall.va_req_aes_EncryptBlockBEStdcall",
        "equation_X64.Vale.Decls.va_state_eq",
        "equation_X64.Vale.Decls.validSrcAddrs128",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "unit_typing"
      ],
      0,
      "9505cddd6c2680acac9a0189f2595852"
    ],
    [
      "X64.AESstdcall.va_lemma_aes_EncryptBlockBEStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "equality_tok_X64.Machine_s.R8@tok",
        "equality_tok_X64.Machine_s.Rcx@tok",
        "equality_tok_X64.Machine_s.Rdi@tok",
        "equality_tok_X64.Machine_s.Rdx@tok",
        "equality_tok_X64.Machine_s.Rsi@tok",
        "equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.nat",
        "equation_Types_s.quad32", "equation_Words_s.nat64",
        "equation_Words_s.natN", "equation_X64.Vale.Decls.validSrcAddrs128",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "proj_equation_X64.Vale.State.Mkstate_mem",
        "proj_equation_X64.Vale.State.Mkstate_memTaint",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_43580de98879f60203ee24975ed9b4ab",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_X64.Vale.Regs.sel",
        "typing_X64.Vale.State.__proj__Mkstate__item__regs",
        "typing_tok_X64.Machine_s.R8@tok",
        "typing_tok_X64.Machine_s.Rcx@tok",
        "typing_tok_X64.Machine_s.Rdi@tok",
        "typing_tok_X64.Machine_s.Rdx@tok",
        "typing_tok_X64.Machine_s.Rsi@tok"
      ],
      0,
      "fad45ab5c26ae68636bf5edc60fbd03a"
    ],
    [
      "X64.AESstdcall.va_wp_aes_EncryptBlockBEStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "equation_Prims.nat", "equation_Words_s.nat64",
        "equation_Words_s.natN", "equation_X64.Vale.Decls.va_if",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Words_s.nat64",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad",
        "typing_X64.AES256_Tm_abs_0b85c5cdf81ff9d981d06a423bf17bd6",
        "typing_X64.AES256_Tm_abs_494c4553ff5247f2c81506c212bacc26",
        "typing_X64.AES256_Tm_abs_50ad851d36622cc25536b7edc233d114",
        "typing_X64.AES256_Tm_abs_86b4602d570d0a24c17faa370bd6d79e",
        "typing_X64.Vale.Decls.va_if", "unit_typing"
      ],
      0,
      "0a684aca25053c7fc1f21d059a39bd71"
    ],
    [
      "X64.AESstdcall.va_wpProof_aes_EncryptBlockBEStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "1912b19572cf393628c6cd7010b32782"
    ]
  ]
]