[
  "ßJpÓµ<\u00173ž\u0004I\u0012€\u0000·â",
  [
    [
      "Spec.Cipher.Expansion.cipher_alg_of_impl",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "disc_equation_Spec.Cipher.Expansion.Hacl_CHACHA20",
        "disc_equation_Spec.Cipher.Expansion.Vale_AES128",
        "disc_equation_Spec.Cipher.Expansion.Vale_AES256",
        "fuel_guarded_inversion_Spec.Cipher.Expansion.impl"
      ],
      0,
      "c09de9cb5bd5b542053ec47147d2faee"
    ]
  ]
]