[
  "\u0001g�\u0003\u0010���L��d�=�",
  [
    [
      "Hacl.Curve25519.Finv.Field51.fsquare_times_51",
      1,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947"
      ],
      0,
      "94da9c6ced6320ee9c5876ff42b99bff"
    ],
    [
      "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,
      "95ebd998b4a8ded4148f25e5eff6607a"
    ],
    [
      "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,
      "dd108570b9894723124b626da25a0781"
    ]
  ]
]