[
  "�uu��(\u0003�r\u001f���O��",
  [
    [
      "Spec.Ed25519.size_signature",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "076a7139a1bf669d7eead83703f17ed5"
    ],
    [
      "Spec.Ed25519.q",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Prims.pos", "int_typing",
        "lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
        "lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Prims.pow2"
      ],
      0,
      "5fbbc4a402bf2251dc7267ffbde4c71b"
    ],
    [
      "Spec.Ed25519.uu___3",
      1,
      0,
      0,
      [ "@query" ],
      0,
      "4e3fbcf61427ad103da8f2ea30a90b6f"
    ],
    [
      "Spec.Ed25519.sha512_modq",
      1,
      0,
      0,
      [
        "@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_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Ed25519.q", "equation_Spec.Ed25519.uu___3",
        "function_token_typing_Spec.Ed25519.uu___3", "int_typing",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_207bd418030414c32f7ebbc47cc48626",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_5532993ae861c7493a5a7d376b36db45",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Prims.pow2"
      ],
      0,
      "8be8b8107496b93af6b0439a409dacfb"
    ],
    [
      "Spec.Ed25519.aff_point_add_c",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Spec.Ed25519.aff_point_c",
        "refinement_interpretation_Tm_refine_30ebfcd9193ad561f2f74576fbc2006b"
      ],
      0,
      "41ed90206edc69a9564eb70d3921456c"
    ],
    [
      "Spec.Ed25519.mk_ed25519_comm_monoid",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fadd",
        "equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.fsub",
        "equation_Spec.Curve25519.one",
        "equation_Spec.Curve25519.op_Plus_Percent",
        "equation_Spec.Curve25519.op_Star_Percent",
        "equation_Spec.Curve25519.op_Subtraction_Percent",
        "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero",
        "equation_Spec.Ed25519.PointOps.aff_point_at_infinity",
        "equation_Spec.Ed25519.PointOps.d",
        "equation_Spec.Ed25519.PointOps.is_on_curve",
        "equation_Spec.Ed25519.aff_point_add_c", "int_inversion",
        "int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Spec.Curve25519.prime"
      ],
      0,
      "919d7a5b4fb26e20613d25abb6db64bf"
    ],
    [
      "Spec.Ed25519.mk_to_ed25519_comm_monoid",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Spec.Ed25519.PointOps.point_inv",
        "equation_Spec.Ed25519.ext_point_c",
        "refinement_interpretation_Tm_refine_8e8b14377c219c89567160ddac81bf0d"
      ],
      0,
      "0a2272be64e334eefb9e7f7cf69853bd"
    ],
    [
      "Spec.Ed25519.point_at_inifinity_c",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "equation_Prims.nat", "equation_Spec.Curve25519.elem",
        "equation_Spec.Curve25519.fadd", "equation_Spec.Curve25519.fmul",
        "equation_Spec.Curve25519.fsub", "equation_Spec.Curve25519.one",
        "equation_Spec.Curve25519.op_Plus_Percent",
        "equation_Spec.Curve25519.op_Star_Percent",
        "equation_Spec.Curve25519.op_Subtraction_Percent",
        "equation_Spec.Curve25519.prime", "equation_Spec.Curve25519.zero",
        "equation_Spec.Ed25519.PointOps.aff_point_at_infinity",
        "equation_Spec.Ed25519.PointOps.d",
        "equation_Spec.Ed25519.PointOps.finv",
        "equation_Spec.Ed25519.PointOps.is_ext",
        "equation_Spec.Ed25519.PointOps.is_on_curve",
        "equation_Spec.Ed25519.PointOps.op_Slash_Percent",
        "equation_Spec.Ed25519.PointOps.point_at_infinity",
        "equation_Spec.Ed25519.PointOps.point_inv",
        "equation_Spec.Ed25519.PointOps.to_aff_point",
        "equation_Spec.Ed25519.aff_point_c",
        "equation_Spec.Ed25519.ext_point_c",
        "equation_Spec.Ed25519.mk_ed25519_comm_monoid",
        "equation_Spec.Ed25519.mk_to_ed25519_comm_monoid", "int_inversion",
        "int_typing",
        "interpretation_Tm_abs_2e59c19b0e31c9a4db502c4a7b790622",
        "lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "proj_equation_Lib.Exponentiation.Mkcomm_monoid_one",
        "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid",
        "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_refl",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__4",
        "projection_inverse_Lib.Exponentiation.Mkcomm_monoid_one",
        "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_a_spec",
        "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid",
        "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_refl",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655",
        "token_correspondence_Spec.Exponentiation.__proj__Mkto_comm_monoid__item__refl",
        "typing_Spec.Curve25519.one",
        "typing_Spec.Curve25519.op_Star_Percent",
        "typing_Spec.Curve25519.zero", "typing_Spec.Ed25519.PointOps.finv"
      ],
      0,
      "9852c6c82f1936bed912f25ca0daad4b"
    ],
    [
      "Spec.Ed25519.point_add_c",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Spec.Curve25519.elem",
        "equation_Spec.Ed25519.PointOps.ext_point",
        "equation_Spec.Ed25519.PointOps.to_aff_point",
        "equation_Spec.Ed25519.aff_point_add_c",
        "equation_Spec.Ed25519.aff_point_c",
        "equation_Spec.Ed25519.ext_point_c",
        "equation_Spec.Ed25519.mk_ed25519_comm_monoid",
        "equation_Spec.Ed25519.mk_to_ed25519_comm_monoid",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple4",
        "interpretation_Tm_abs_2e59c19b0e31c9a4db502c4a7b790622",
        "proj_equation_Lib.Exponentiation.Mkcomm_monoid_mul",
        "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_a_spec",
        "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid",
        "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_refl",
        "projection_inverse_Lib.Exponentiation.Mkcomm_monoid_mul",
        "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_a_spec",
        "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid",
        "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_refl",
        "refinement_interpretation_Tm_refine_8e8b14377c219c89567160ddac81bf0d",
        "token_correspondence_Lib.Exponentiation.__proj__Mkcomm_monoid__item__mul",
        "token_correspondence_Spec.Ed25519.aff_point_add_c",
        "token_correspondence_Spec.Exponentiation.__proj__Mkto_comm_monoid__item__refl"
      ],
      0,
      "c981c4f0aa8a54a95b3ecdf88f40bc3e"
    ],
    [
      "Spec.Ed25519.point_double_c",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Spec.Curve25519.elem",
        "equation_Spec.Ed25519.PointOps.ext_point",
        "equation_Spec.Ed25519.PointOps.to_aff_point",
        "equation_Spec.Ed25519.aff_point_add_c",
        "equation_Spec.Ed25519.aff_point_c",
        "equation_Spec.Ed25519.ext_point_c",
        "equation_Spec.Ed25519.mk_ed25519_comm_monoid",
        "equation_Spec.Ed25519.mk_to_ed25519_comm_monoid",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple4",
        "interpretation_Tm_abs_2e59c19b0e31c9a4db502c4a7b790622",
        "proj_equation_Lib.Exponentiation.Mkcomm_monoid_mul",
        "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_a_spec",
        "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid",
        "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_refl",
        "projection_inverse_Lib.Exponentiation.Mkcomm_monoid_mul",
        "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_a_spec",
        "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid",
        "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_refl",
        "refinement_interpretation_Tm_refine_8e8b14377c219c89567160ddac81bf0d",
        "token_correspondence_Lib.Exponentiation.__proj__Mkcomm_monoid__item__mul",
        "token_correspondence_Spec.Ed25519.aff_point_add_c",
        "token_correspondence_Spec.Exponentiation.__proj__Mkto_comm_monoid__item__refl"
      ],
      0,
      "d0976755faefc9d1a29842a9a4f55a05"
    ],
    [
      "Spec.Ed25519.point_mul",
      1,
      0,
      1,
      [
        "@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", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "2e72110598408386227d5600500b2d66"
    ],
    [
      "Spec.Ed25519.point_mul",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
      ],
      0,
      "5e6250468af41fd9d25bce33c6e5caa8"
    ],
    [
      "Spec.Ed25519.point_mul_double",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "adade319a0fd0fda475f1efde6670a91"
    ],
    [
      "Spec.Ed25519.point_mul_double",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.Sequence.length",
        "equation_Lib.Sequence.lseq", "primitive_Prims.op_Multiply",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
      ],
      0,
      "ff0c87eb9ea7bb2fc40997bc6bd47b23"
    ],
    [
      "Spec.Ed25519.point_mul_g",
      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", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "11cf7febfe189056c9a89bc40d46da56"
    ],
    [
      "Spec.Ed25519.point_mul_g",
      2,
      0,
      0,
      [ "@query" ],
      0,
      "8143098efa238ddd1ec235f16aab76aa"
    ],
    [
      "Spec.Ed25519.point_mul_double_g",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "13dee20166c081f6b8146fb5ba392621"
    ],
    [
      "Spec.Ed25519.point_mul_double_g",
      2,
      0,
      0,
      [ "@query" ],
      0,
      "3507810bf8899ada69aa5566ddfac7d3"
    ],
    [
      "Spec.Ed25519.point_negate_mul_double_g",
      1,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "ee57c63dadf780e00980bb16920744ef"
    ],
    [
      "Spec.Ed25519.point_negate_mul_double_g",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Spec.Ed25519.ext_point_c",
        "refinement_interpretation_Tm_refine_8e8b14377c219c89567160ddac81bf0d"
      ],
      0,
      "f462a3963c71fbb372c07606134366da"
    ],
    [
      "Spec.Ed25519.secret_expand",
      1,
      0,
      1,
      [
        "@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", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "87ee60e7f8b91783053aa1cff56061ee"
    ],
    [
      "Spec.Ed25519.secret_expand",
      2,
      0,
      0,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.SHA2_512",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equality_tok_Spec.Hash.Definitions.SHA2_512@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
        "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
        "equation_Prims.nat", "equation_Spec.Ed25519.uu___3",
        "equation_Spec.Hash.Definitions.hash_length",
        "equation_Spec.Hash.Definitions.hash_word_length",
        "equation_Spec.Hash.Definitions.word_length",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Prims.int",
        "function_token_typing_Spec.Ed25519.uu___3",
        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
        "refinement_interpretation_Tm_refine_5532993ae861c7493a5a7d376b36db45",
        "refinement_interpretation_Tm_refine_80ed6594583be7bfc561d383b2f6a594",
        "refinement_interpretation_Tm_refine_8730279488c06d61e0e641290ce1a75f",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length",
        "typing_Spec.Hash.Definitions.hash_word_length",
        "typing_tok_Spec.Hash.Definitions.SHA2_512@tok"
      ],
      0,
      "8290d52faa801b501970e6b625caaa30"
    ],
    [
      "Spec.Ed25519.secret_to_public",
      1,
      0,
      1,
      [
        "@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", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "c97fd8c8d3a9fb5dbee523417bb902a6"
    ],
    [
      "Spec.Ed25519.secret_to_public",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "function_token_typing_Lib.IntTypes.uint8",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "49509f572dbeed275e36564b076d65d2"
    ],
    [
      "Spec.Ed25519.expand_keys",
      1,
      0,
      1,
      [
        "@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", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "78d1da71c3aff064581765c7eaab233e"
    ],
    [
      "Spec.Ed25519.expand_keys",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
        "function_token_typing_Lib.IntTypes.uint8",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_FStar.Seq.Base.length"
      ],
      0,
      "d655957f97d1870dbb53f7a38144ff8d"
    ],
    [
      "Spec.Ed25519.sign_expanded",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "7fa54488a02b6d387de5b997f125d7f0"
    ],
    [
      "Spec.Ed25519.sign_expanded",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "2bb0f96adcf01dbd22908cdd50fb16c6"
    ],
    [
      "Spec.Ed25519.sign_expanded",
      3,
      0,
      1,
      [
        "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.uint8",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
        "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Ed25519.q",
        "function_token_typing_Lib.IntTypes.uint8", "int_typing",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_17713ec4e2d60d843c8185eafd3cd425",
        "refinement_interpretation_Tm_refine_207bd418030414c32f7ebbc47cc48626",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
        "typing_Lib.Sequence.length", "typing_Prims.pow2",
        "typing_Spec.Ed25519.q"
      ],
      0,
      "18dd0efafc7899cad0349600219f0000"
    ],
    [
      "Spec.Ed25519.sign",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "ff7cc6d6901e869f76bbfc3c597b8e14"
    ],
    [
      "Spec.Ed25519.sign",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "8d05745b12495d5e3604dc1f3ff1f999"
    ],
    [
      "Spec.Ed25519.sign",
      3,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint8",
        "equation_Lib.Sequence.length", "equation_Prims.nat",
        "function_token_typing_Lib.IntTypes.uint8",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_17713ec4e2d60d843c8185eafd3cd425",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.Sequence.length"
      ],
      0,
      "c6206dd6b0270ad2ffa5107c72ff2f2d"
    ],
    [
      "Spec.Ed25519.verify",
      1,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "45185bb8a3a2a2ed94cc08e44a1119bb"
    ],
    [
      "Spec.Ed25519.verify",
      2,
      0,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "e0d181d1f97f795920deb79a2378c8a1"
    ],
    [
      "Spec.Ed25519.verify",
      3,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "disc_equation_FStar.Pervasives.Native.None",
        "disc_equation_FStar.Pervasives.Native.Some",
        "equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
        "equation_Lib.Sequence.to_seq", "equation_Prims.nat",
        "equation_Spec.Ed25519.PointOps.ext_point",
        "equation_Spec.Ed25519.PointOps.point_decompress",
        "function_token_typing_Lib.IntTypes.uint8",
        "function_token_typing_Spec.Ed25519.PointOps.ext_point",
        "int_inversion", "lemma_FStar.Pervasives.invertOption",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "proj_equation_FStar.Pervasives.Native.Some_v",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Some_v",
        "refinement_interpretation_Tm_refine_16821415cff3e26a29565708d9381b53",
        "refinement_interpretation_Tm_refine_17713ec4e2d60d843c8185eafd3cd425",
        "refinement_interpretation_Tm_refine_26808d9b5746d8f80ebb81854f3ae9fd",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_9f755b6068c8b6f04a61ef4a1b1c1460",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
        "refinement_interpretation_Tm_refine_fe5303c195067f5e9275341f3c732ab0",
        "typing_Lib.Sequence.length",
        "typing_Spec.Ed25519.PointOps.point_decompress"
      ],
      0,
      "adcfc2bdf0b9fc26e1c2e19e2fc1ea82"
    ]
  ]
]