[
  "\u000e\u0004‰\r†æd6\u001e/€Äl&\u001aB",
  [
    [
      "Spec.Ed25519.Lemmas.point_decompress_lemma",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "ab5a57679276a0ff45fa535ada5ac6ac"
    ],
    [
      "Spec.Ed25519.Lemmas.fpow_is_pow_mod",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Curve25519.prime", "int_typing",
        "lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
      ],
      0,
      "4fe7fe8d4052e905aea032a13ab77154"
    ]
  ]
]