[
  ";©xg*Ã|$¹W»\u001b.‘Æ\u001b",
  [
    [
      "Vale.AES.X64.AESCTR.aes_reqs",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "4c976d2ae6745639814bd00daa76a499"
    ],
    [
      "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_0da5357929f39222388a84d9bf1a11af",
        "typing_tok_Vale.AES.AES_s.AES_128@tok"
      ],
      0,
      "29454c76615a9a9785e02e592bde9095"
    ],
    [
      "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,
      "619209e4fe22b7bcb47fc20b57c8686a"
    ],
    [
      "Vale.AES.X64.AESCTR.va_quick_Aes_ctr_encrypt",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "c20b026cf4e408ca49e36024be55fae5"
    ],
    [
      "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.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_38dd10336a6ef505252f645bc0e9fe22",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.Lib.Map16.sel",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
      ],
      0,
      "fd8c3ca38977e78422bace11945222a9"
    ],
    [
      "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.Secret@tok",
        "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
        "equation_Vale.Arch.HeapImpl.vale_heaplets",
        "equation_Vale.X64.Decls.va_upd_flags",
        "equation_Vale.X64.Decls.va_upd_mem",
        "equation_Vale.X64.Decls.va_upd_mem_heaplet",
        "equation_Vale.X64.Decls.va_upd_reg64",
        "equation_Vale.X64.Decls.va_upd_xmm",
        "equation_Vale.X64.Decls.validSrcAddrs",
        "equation_Vale.X64.Decls.validSrcAddrs128",
        "equation_Vale.X64.Memory.base_typ_as_vale_type",
        "equation_Vale.X64.Memory.buffer128",
        "equation_Vale.X64.Memory.set_vale_heap",
        "equation_Vale.X64.State.update_reg",
        "equation_Vale.X64.State.update_reg_64",
        "equation_Vale.X64.State.update_reg_xmm",
        "function_token_typing_Vale.Arch.HeapImpl.vale_heap", "int_typing",
        "lemma_Vale.Lib.Map16.lemma_self",
        "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
        "primitive_Prims.op_LessThanOrEqual",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_ok",
        "proj_equation_Vale.X64.State.Mkvale_state_vs_regs",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
        "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap",
        "typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
        "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
        "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
      ],
      0,
      "a6c675fd61f10deefb81068c6175865c"
    ],
    [
      "Vale.AES.X64.AESCTR.va_quick_Aes_counter_loop",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "21e9ca8d8fbc5fed300631f0ac74cfb1"
    ]
  ]
]