[
  "?»8‰Ÿa²v/¨Sä\u0012 ^Ã",
  [
    [
      "Spec.CTR.block_cipher_ctx",
      1,
      0,
      0,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
        "equation_Prims.pos",
        "haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "haseqTm_refine_f048236b5f8051f83b495ea5eaa6127b"
      ],
      0
    ],
    [
      "Spec.CTR.xor",
      1,
      0,
      0,
      [
        "@query", "equation_FStar.UInt8.t", "equation_Prims.nat",
        "equation_Spec.Lib.lbytes",
        "refinement_interpretation_Tm_refine_048b9486a1812f3d14140323cda6696c",
        "refinement_interpretation_Tm_refine_d70501a9ebd0660fc59c3349dad118ea"
      ],
      0
    ],
    [
      "Spec.CTR.counter_mode",
      1,
      0,
      0,
      [
        "@query", "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "typing_Spec.CTR.__proj__Mkblock_cipher_ctx__item__blocklen"
      ],
      0
    ],
    null,
    [
      "Spec.CTR.counter_mode",
      3,
      0,
      0,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ]
  ]
]