[
  "\u0001g¡\u0003\u0010üÈÍLè—æd‘=”",
  [
    [
      "Hacl.Curve25519.Finv.Field51.fsquare_times_51",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947"
      ],
      0,
      "174a4f34fc7874a28833c70a003d6ed2"
    ],
    [
      "Hacl.Curve25519.Finv.Field51.finv_51",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Spec.Curve25519.prime", "int_typing",
        "lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "8b52b67852307bac170502f71fe2d810"
    ],
    [
      "Hacl.Curve25519.Finv.Field51.finv_51",
      2,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M51",
        "equality_tok_Hacl.Impl.Curve25519.Fields.Core.M51@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_Hacl.Impl.Curve25519.Fields.Core.felem",
        "equation_Hacl.Impl.Curve25519.Fields.Core.felem_wide2",
        "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.IntTypes.uint128", "equation_Lib.IntTypes.uint64",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint64",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "refinement_interpretation_Tm_refine_5064087b76eb6f995808483f3366af91",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_e4ea1e84380edcecf7c70a639d08b578",
        "typing_Lib.Buffer.loc", "typing_tok_Lib.Buffer.MUT@tok"
      ],
      0,
      "0a2493815dab4a6e89943a6b37be5541"
    ]
  ]
]