[
  "�A�x�\u000ed����N\u0005�5�",
  [
    [
      "Hacl.Spec.Curve25519.AddAndDouble.add_and_double1_1",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Spec.Curve25519.prime", "int_typing",
        "lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "1ba0ab27b9d63cdfb23cf2817ae34cf4"
    ],
    [
      "Hacl.Spec.Curve25519.AddAndDouble.lemma_add_and_double",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Spec.Curve25519.AddAndDouble.add_and_double1",
        "equation_Hacl.Spec.Curve25519.AddAndDouble.add_and_double1_0",
        "equation_Hacl.Spec.Curve25519.AddAndDouble.add_and_double1_1",
        "equation_Spec.Curve25519.add_and_double",
        "equation_Spec.Curve25519.elem",
        "equation_Spec.Curve25519.op_Plus_Percent",
        "equation_Spec.Curve25519.op_Subtraction_Percent",
        "equation_Spec.Curve25519.proj_point",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2"
      ],
      0,
      "862a72ee13c426f02ae95e43bcddc926"
    ],
    [
      "Hacl.Spec.Curve25519.AddAndDouble.montgomery_ladder1_0",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S32",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "25dd283de1fc140d624efc81f4bb7bb3"
    ],
    [
      "Hacl.Spec.Curve25519.AddAndDouble.lemma_montgomery_ladder",
      1,
      2,
      1,
      [
        "@query",
        "equation_Hacl.Spec.Curve25519.AddAndDouble.montgomery_ladder1",
        "equation_Hacl.Spec.Curve25519.AddAndDouble.montgomery_ladder1_0",
        "equation_Hacl.Spec.Curve25519.AddAndDouble.montgomery_ladder1_1",
        "equation_Hacl.Spec.Curve25519.AddAndDouble.montgomery_ladder1_2",
        "equation_Spec.Curve25519.montgomery_ladder",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple3__3"
      ],
      0,
      "c851292323a24819165450c9383ca159"
    ]
  ]
]