[
  "���w�Ar�\u0000בi'c�",
  [
    [
      "Cipher16.state",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Cipher16.alg",
        "equation_Spec.Cipher16.slen",
        "fuel_guarded_inversion_Spec.Cipher16.alg",
        "projection_inverse_BoxInt_proj_0"
      ],
      0,
      "66eca0f549df23b13127bf9b48ce037e"
    ],
    [
      "Cipher16.create",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Cipher16.alg",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_Spec.Cipher16.keylen",
        "fuel_guarded_inversion_Spec.Cipher16.alg",
        "function_token_typing_FStar.UInt8.t",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_243a7d40b15057dd63f99047fa727153",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "687e335a813226216e0ba11409f448db"
    ],
    [
      "Cipher16.compute",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "function_token_typing_FStar.UInt8.t",
        "lemma_LowStar.Monotonic.Buffer.length_as_seq",
        "refinement_interpretation_Tm_refine_352f29f5b291d9b891739cdac915fa8c",
        "typing_LowStar.Buffer.trivial_preorder"
      ],
      0,
      "fcac5d2d6da15079c57db33baf58140f"
    ]
  ]
]