[
  "LHë‡åðý\u0001W§‘ü!i®æ",
  [
    [
      "Hacl.Spec.Bignum.ModInv64.mod_inv_u64_lemma",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "b52dc2775dda5a02e30e01ffde986bb2"
    ]
  ]
]