[
  "\u0012�M�i\\�\u0017�WO���,\u007f",
  [
    [
      "Vale.AES.X64.AESCTR.aes_reqs",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "750f1d0e197e0a9e34186c63228aa840"
    ],
    [
      "Vale.AES.X64.AESCTR.va_lemma_aes_ctr_encrypt",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equation_Vale.AES.X64.AESCTR.aes_reqs",
        "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",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_11362bdf3ed796137da93085480dc30a",
        "typing_tok_Vale.AES.AES_s.AES_128@tok"
      ],
      0,
      "048f7a2137ca2650924047b2ec63cfa9"
    ],
    [
      "Vale.AES.X64.AESCTR.va_wp_aes_ctr_encrypt",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Vale.AES.AES_s_pretyping_35779122094374fadf807bdd7bfc8013",
        "constructor_distinct_Vale.AES.AES_s.AES_128",
        "constructor_distinct_Vale.AES.AES_s.AES_256",
        "equality_tok_Vale.AES.AES_s.AES_128@tok",
        "equality_tok_Vale.AES.AES_s.AES_256@tok",
        "equation_Vale.AES.X64.AESCTR.aes_reqs",
        "primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "typing_tok_Vale.AES.AES_s.AES_128@tok"
      ],
      0,
      "61f331f4916385a4a1a66d0d5758f979"
    ],
    [
      "Vale.AES.X64.AESCTR.va_quick_aes_ctr_encrypt",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "f70a02947cdfb1a1ffc55a90b682d033"
    ],
    [
      "Vale.AES.X64.AESCTR.va_lemma_aes_counter_loop",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok",
        "equation_Vale.Arch.HeapImpl.vale_heap_impl",
        "equation_Vale.X64.Decls.validDstAddrs128",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.Memory.get_vale_heap",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_e97dbe20fae743ebcc000324c0b92548",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
      ],
      0,
      "bb22f3e2cbbccf6b1de4fd04a87126fd"
    ],
    [
      "Vale.AES.X64.AESCTR.va_wp_aes_counter_loop",
      1,
      1,
      0,
      [
        "@query", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
        "equality_tok_Vale.X64.Machine_s.Secret@tok",
        "equation_Vale.Arch.HeapImpl.vale_heap_impl",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.Memory.get_vale_heap",
        "equation_Vale.X64.Memory.set_vale_heap",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
      ],
      0,
      "b9c27e538870cfd1ff27f03d2ce8d373"
    ],
    [
      "Vale.AES.X64.AESCTR.va_quick_aes_counter_loop",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "5fbecc4ba3884165173f146452a02533"
    ]
  ]
]