[
  "8äpń·üOť\u001b3E¶ołş'",
  [
    [
      "Curve25519.crypto_scalarmult",
      1,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Curve25519.crypto_scalarmult",
      2,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Curve25519.crypto_scalarmult",
      3,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Curve25519.crypto_scalarmult",
      4,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Curve25519.op_String_Access",
        "equation_Curve25519.uint8_p", "equation_FStar.Buffer.buffer",
        "equation_FStar.UInt8.t",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.HyperStack.mem",
        "kinding_FStar.UInt8.t_@tok",
        "refinement_interpretation_Curve25519_Tm_refine_94403ae1db118a2daa8d61fa9d371d82",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "typing_FStar.Buffer.as_seq"
      ],
      0
    ],
    [
      "Curve25519.crypto_scalarmult",
      5,
      0,
      1,
      [ "@query", "equation_Curve25519.op_String_Access" ],
      0
    ]
  ]
]