[
  "���\u0004������V�����",
  [
    [
      "Vale.AES.X64.AES128.va_lemma_KeyExpansion128Stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
        "refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
      ],
      0,
      "6e8d953f43c919bfb9425dd7d81dabf7"
    ],
    [
      "Vale.AES.X64.AES128.va_wp_KeyExpansion128Stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "eq2-interp",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
        "equation_Vale.AES.AES_s.is_aes_key_LE",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.Def.Types_s.quad32",
        "equation_Vale.Def.Words.Seq_s.seq4",
        "equation_Vale.Def.Words.Seq_s.seqn",
        "equation_Vale.Def.Words_s.nat32",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "fuel_guarded_inversion_Vale.X64.State.vale_state",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap",
        "function_token_typing_Vale.Def.Words_s.nat32", "int_typing",
        "refinement_interpretation_Tm_refine_4543f1a564a33b21cd018d4b2bc02996",
        "refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Def.Words.Seq_s.four_to_seq_LE",
        "typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Memory.buffer_read",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
      ],
      0,
      "564243dd6fed2786ed93b225f596b99b"
    ],
    [
      "Vale.AES.X64.AES128.va_quick_KeyExpansion128Stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "72211ad20fed2ad35f1bd9097ea75a0b"
    ],
    [
      "Vale.AES.X64.AES128.va_lemma_AES128EncryptBlock",
      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_74ee5d51291f0d079b5e144e2ec88f64"
      ],
      0,
      "452cbdf4a32d00bde5f6f1da05d652c3"
    ],
    [
      "Vale.AES.X64.AES128.va_wp_AES128EncryptBlock",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "5a809e746b5a1f861aa15a5c0f21b661"
    ],
    [
      "Vale.AES.X64.AES128.va_quick_AES128EncryptBlock",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "4e1e20d4b73b289204cefd5e34ae011f"
    ],
    [
      "Vale.AES.X64.AES128.va_lemma_AES128EncryptBlockStdcall",
      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_0304b872cb88ace5290519d2df90385f",
        "refinement_interpretation_Tm_refine_4d38686bf695f79f110ce5aef057279f"
      ],
      0,
      "cf851da09c6881b52f525029a4260056"
    ],
    [
      "Vale.AES.X64.AES128.va_wp_AES128EncryptBlockStdcall",
      1,
      1,
      0,
      [ "@query", "projection_inverse_BoxInt_proj_0" ],
      0,
      "5f45ef7c1218c85dee781c83e609de4f"
    ],
    [
      "Vale.AES.X64.AES128.va_quick_AES128EncryptBlockStdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "54ca9c142b5b63fd3dbed9979842cb6a"
    ]
  ]
]