[
  "�DFE\u0002�\u001d=j�w�伤�",
  [
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "7402176fc4ac54ff90b302db41bc74c4"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.get_x",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat", "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_847b35cdbc4d3703552d4865eba7d025",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_Lib.IntTypes.uint_v", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "bbeddf942079fb4c966373a4508785d4"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.get_z",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat", "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_847b35cdbc4d3703552d4865eba7d025",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "b7c00c4885efb952eb640eb8933cff6f"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.fget_x",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat", "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_847b35cdbc4d3703552d4865eba7d025",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_Lib.IntTypes.uint_v", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "c29bf976d7c132212178b95119e7b98e"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.fget_z",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat", "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_847b35cdbc4d3703552d4865eba7d025",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "254613230480802112584433891ad541"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_tmp_inv_t",
      1,
      1,
      1,
      [
        "@MaxIFuel_assumption", "@query", "bool_inversion",
        "disc_equation_Hacl.Impl.Curve25519.Fields.M51",
        "disc_equation_Hacl.Impl.Curve25519.Fields.M64",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_Hacl.Impl.Curve25519.Fields.felem",
        "equation_Lib.Buffer.lbuffer_t",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "lemma_FStar.Map.lemma_ContainsDom",
        "projection_inverse_BoxBool_proj_0",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip"
      ],
      0,
      "7a731202c22bb308e0d836c1eae17365"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_add_and_double0",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Hacl.Impl.Curve25519.Fields.field_spec__uu___haseq",
        "b2t_def", "bool_inversion", "bool_typing",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point",
        "equation_Hacl.Impl.Curve25519.Fields.felem_wide2",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.op_Star_Bang",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma",
        "lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
        "refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.mul",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "token_correspondence_Lib.IntTypes.op_Star_Bang",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "d6bdcfb578eb90513b8c0d26d19dbdf6"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_add_and_double0",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "2c481e55930a8fdf99d85825ed2ea7bf"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_add_and_double0",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_interpretation_Tm_arrow_69980de4b69ce434f89b12e4cb716d05",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Hacl.Impl.Curve25519.Fields.M64@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.fget_x",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.fget_xz",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.fget_z",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.get_x",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.get_z",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point_tmp_inv_t",
        "equation_Hacl.Impl.Curve25519.Field51.as_felem",
        "equation_Hacl.Impl.Curve25519.Field51.as_nat",
        "equation_Hacl.Impl.Curve25519.Field51.felem",
        "equation_Hacl.Impl.Curve25519.Field51.felem_fits",
        "equation_Hacl.Impl.Curve25519.Field51.mul_inv_t",
        "equation_Hacl.Impl.Curve25519.Field64.Core.as_nat",
        "equation_Hacl.Impl.Curve25519.Fields.as_nat",
        "equation_Hacl.Impl.Curve25519.Fields.fadd_fsub_pre",
        "equation_Hacl.Impl.Curve25519.Fields.fadd_post",
        "equation_Hacl.Impl.Curve25519.Fields.felem_wide2",
        "equation_Hacl.Impl.Curve25519.Fields.feval",
        "equation_Hacl.Impl.Curve25519.Fields.fmul2_fsqr2_post",
        "equation_Hacl.Impl.Curve25519.Fields.fmul2_pre",
        "equation_Hacl.Impl.Curve25519.Fields.fmul_pre",
        "equation_Hacl.Impl.Curve25519.Fields.fsqr2_pre",
        "equation_Hacl.Impl.Curve25519.Fields.fsub_post",
        "equation_Hacl.Impl.Curve25519.Fields.state_inv_t",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.max51",
        "equation_Hacl.Spec.Curve25519.Field51.mul_inv_t",
        "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.gsub",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies",
        "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.op_Plus_Dot",
        "equation_Lib.IntTypes.op_Star_Bang",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint128", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Spec.Curve25519.add", "equation_Spec.Curve25519.elem",
        "equation_Spec.Curve25519.op_Plus_Percent",
        "equation_Spec.Curve25519.op_Star_Percent",
        "equation_Spec.Curve25519.op_Subtraction_Percent",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Hacl.Spec.Curve25519.Field51.Definition.lemma_pow_64_51",
        "function_token_typing_Lib.IntTypes.add_mod",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.Buffer.modifies_sub", "lemma_Lib.IntTypes.add_lemma",
        "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mul_lemma",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_union_comm",
        "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
        "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__5",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
        "refinement_interpretation_Tm_refine_303dbbbbac215a323c33becd5402c469",
        "refinement_interpretation_Tm_refine_44675dbcae4ad9399ed30bb1c7946a13",
        "refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
        "refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_6e0752342dfed3b3058e56e9396850f5",
        "refinement_interpretation_Tm_refine_7f12787f8469a0a16508d2424076f15d",
        "refinement_interpretation_Tm_refine_82b65099892bcd4ee1cd969350ddb986",
        "refinement_interpretation_Tm_refine_847b35cdbc4d3703552d4865eba7d025",
        "refinement_interpretation_Tm_refine_881060f5636c4986dbc297a74f65fa01",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_9e4fe5e2f1756f97f5c5f41ac37c2845",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_abfbc855f1855c1bece906940ccad930",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_b706c37ee15a83b30028d870fb33463b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_bb22381548143d327d79afcf93e90d2f",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.add_mod",
        "token_correspondence_Lib.IntTypes.mul",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "token_correspondence_Lib.IntTypes.op_Plus_Dot",
        "token_correspondence_Lib.IntTypes.op_Star_Bang",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v",
        "typing_Hacl.Impl.Curve25519.AddAndDouble.get_x",
        "typing_Hacl.Impl.Curve25519.AddAndDouble.get_z",
        "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51",
        "typing_Lib.Buffer.gsub", "typing_Lib.Buffer.length",
        "typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar",
        "typing_Lib.IntTypes.add_mod", "typing_Lib.IntTypes.mul",
        "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_LowStar.Monotonic.Buffer.mgsub",
        "typing_X64.CPU_Features_s.adx_enabled",
        "typing_X64.CPU_Features_s.bmi2_enabled",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "49727d541d86935e7160609f2b239052"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_add_and_double1",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_interpretation_Tm_arrow_3075805bd3b44f3280b499ecd8caf607",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Hacl.Impl.Curve25519.Fields.field_spec__uu___haseq",
        "b2t_def", "bool_inversion", "bool_typing",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Hacl.Impl.Curve25519.Fields.M51@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.get_z",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.gsub",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.op_Star_Bang",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Lib.IntTypes.add",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.mul_lemma",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.gsub_is_null",
        "lemma_LowStar.Monotonic.Buffer.len_gsub",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
        "refinement_interpretation_Tm_refine_3e7d6cbf9a788b81a5dd3182e0f2ca67",
        "refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
        "refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_b706c37ee15a83b30028d870fb33463b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.mul",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "token_correspondence_Lib.IntTypes.op_Star_Bang",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v",
        "typing_Hacl.Impl.Curve25519.AddAndDouble.get_z",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.g_is_null",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.mgsub",
        "typing_tok_Hacl.Impl.Curve25519.Fields.M51@tok",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "2fe757f43bba28b93d14062cad390186"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_add_and_double1",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "f7f72920596bd34802823309cd8f7924"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_add_and_double1",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_interpretation_Tm_arrow_69980de4b69ce434f89b12e4cb716d05",
        "Lib.IntTypes_interpretation_Tm_arrow_83846359b5c580ebf2d901d5a0596af0",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Hacl.Impl.Curve25519.Fields.M64@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.fget_x",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.fget_xz",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.fget_z",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.get_x",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.get_z",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point_tmp_inv_t",
        "equation_Hacl.Impl.Curve25519.Field51.as_felem",
        "equation_Hacl.Impl.Curve25519.Field51.as_nat",
        "equation_Hacl.Impl.Curve25519.Field51.felem_fits",
        "equation_Hacl.Impl.Curve25519.Field51.mul_inv_t",
        "equation_Hacl.Impl.Curve25519.Field64.Core.as_nat",
        "equation_Hacl.Impl.Curve25519.Fields.as_nat",
        "equation_Hacl.Impl.Curve25519.Fields.fadd_fsub_pre",
        "equation_Hacl.Impl.Curve25519.Fields.fadd_post",
        "equation_Hacl.Impl.Curve25519.Fields.felem_wide2",
        "equation_Hacl.Impl.Curve25519.Fields.feval",
        "equation_Hacl.Impl.Curve25519.Fields.fmul1_pre",
        "equation_Hacl.Impl.Curve25519.Fields.fmul2_fsqr2_post",
        "equation_Hacl.Impl.Curve25519.Fields.fmul2_pre",
        "equation_Hacl.Impl.Curve25519.Fields.fsqr2_pre",
        "equation_Hacl.Impl.Curve25519.Fields.fsub_post",
        "equation_Hacl.Impl.Curve25519.Fields.state_inv_t",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.max51",
        "equation_Hacl.Spec.Curve25519.Field51.mul_inv_t",
        "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.gsub",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies",
        "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.op_Plus_Dot",
        "equation_Lib.IntTypes.op_Star_Bang",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint128", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Spec.Curve25519.double", "equation_Spec.Curve25519.elem",
        "equation_Spec.Curve25519.op_Plus_Percent",
        "equation_Spec.Curve25519.op_Star_Percent",
        "equation_Spec.Curve25519.op_Subtraction_Percent",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Hacl.Spec.Curve25519.Field51.Definition.lemma_pow_64_51",
        "function_token_typing_Lib.IntTypes.add_mod",
        "function_token_typing_Lib.IntTypes.mul",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.Buffer.modifies_sub", "lemma_Lib.IntTypes.add_lemma",
        "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mul_lemma",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.gsub_gsub",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_union_comm",
        "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
        "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__5",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
        "refinement_interpretation_Tm_refine_303dbbbbac215a323c33becd5402c469",
        "refinement_interpretation_Tm_refine_3caca10744a02e94ade352198adc6d62",
        "refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
        "refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
        "refinement_interpretation_Tm_refine_53f0a85cea67593aeb290e09115f43db",
        "refinement_interpretation_Tm_refine_590b8e485b7d51c978dd811a74a85d9e",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_6e0752342dfed3b3058e56e9396850f5",
        "refinement_interpretation_Tm_refine_82b65099892bcd4ee1cd969350ddb986",
        "refinement_interpretation_Tm_refine_847b35cdbc4d3703552d4865eba7d025",
        "refinement_interpretation_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_Tm_refine_9918c305a2eac13fb45cee4b8bcdf9cd",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_a9a80ef2a511c8fb06ad2cc272062b5e",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_b706c37ee15a83b30028d870fb33463b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_c5f8a6b5af25b27301842abce6ca6c7d",
        "refinement_interpretation_Tm_refine_cc3d2dd476b93d2b20d64200c23c6c04",
        "refinement_interpretation_Tm_refine_cd388606af406d25a6d7024b316ae909",
        "refinement_interpretation_Tm_refine_fb1be1d1726d5678dace30d0f3d47eff",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.add_mod",
        "token_correspondence_Lib.IntTypes.mul",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "token_correspondence_Lib.IntTypes.op_Plus_Dot",
        "token_correspondence_Lib.IntTypes.op_Star_Bang",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
        "typing_Hacl.Impl.Curve25519.AddAndDouble.get_x",
        "typing_Hacl.Impl.Curve25519.AddAndDouble.get_z",
        "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51",
        "typing_Lib.Buffer.gsub", "typing_Lib.Buffer.length",
        "typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar",
        "typing_Lib.Buffer.union", "typing_Lib.IntTypes.add_mod",
        "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_LowStar.Monotonic.Buffer.mgsub",
        "typing_X64.CPU_Features_s.adx_enabled",
        "typing_X64.CPU_Features_s.bmi2_enabled",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "3796f9fff59ae8f83cddb8abe05cc2d4"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_add_and_double_",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_interpretation_Tm_arrow_3075805bd3b44f3280b499ecd8caf607",
        "Lib.IntTypes_interpretation_Tm_arrow_4b8a7e8fecc07184d556939df4311fa6",
        "Lib.IntTypes_interpretation_Tm_arrow_83846359b5c580ebf2d901d5a0596af0",
        "Lib.IntTypes_interpretation_Tm_arrow_c605800875b6adf350acbdf637102661",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Hacl.Impl.Curve25519.Fields.field_spec__uu___haseq",
        "b2t_def", "bool_inversion", "bool_typing",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point",
        "equation_Hacl.Impl.Curve25519.Fields.felem_wide2",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.gsub",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.op_Plus_Dot",
        "equation_Lib.IntTypes.op_Star_Bang",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Lib.IntTypes.add",
        "function_token_typing_Lib.IntTypes.mul",
        "function_token_typing_Lib.IntTypes.op_Plus_Bang",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma",
        "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mul_lemma",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
        "refinement_interpretation_Tm_refine_3e7d6cbf9a788b81a5dd3182e0f2ca67",
        "refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_b706c37ee15a83b30028d870fb33463b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.add_mod",
        "token_correspondence_Lib.IntTypes.mul",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "token_correspondence_Lib.IntTypes.op_Plus_Dot",
        "token_correspondence_Lib.IntTypes.op_Star_Bang",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "f291a7d2e34562aa662b08d6b171b7c4"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_add_and_double_",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "f7d11ca0e802216b28c9088a516b613d"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_add_and_double_",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_interpretation_Tm_arrow_3075805bd3b44f3280b499ecd8caf607",
        "Lib.IntTypes_interpretation_Tm_arrow_49f388450e5cfc91da46292c2a5d5b7b",
        "Lib.IntTypes_interpretation_Tm_arrow_69980de4b69ce434f89b12e4cb716d05",
        "Lib.IntTypes_interpretation_Tm_arrow_78f083cf1c0c989cac96323dae7f10ad",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Hacl.Impl.Curve25519.Fields.M64@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.fget_x",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.fget_xz",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.fget_z",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.get_x",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.get_z",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point_tmp_inv_t",
        "equation_Hacl.Impl.Curve25519.Field51.as_felem",
        "equation_Hacl.Impl.Curve25519.Field51.as_nat",
        "equation_Hacl.Impl.Curve25519.Field51.felem_fits",
        "equation_Hacl.Impl.Curve25519.Field51.mul_inv_t",
        "equation_Hacl.Impl.Curve25519.Field64.Core.as_nat",
        "equation_Hacl.Impl.Curve25519.Fields.as_nat",
        "equation_Hacl.Impl.Curve25519.Fields.fadd_fsub_pre",
        "equation_Hacl.Impl.Curve25519.Fields.fadd_post",
        "equation_Hacl.Impl.Curve25519.Fields.felem_wide2",
        "equation_Hacl.Impl.Curve25519.Fields.feval",
        "equation_Hacl.Impl.Curve25519.Fields.fsub_post",
        "equation_Hacl.Impl.Curve25519.Fields.state_inv_t",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.max51",
        "equation_Hacl.Spec.Curve25519.Field51.mul_inv_t",
        "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.gsub",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies",
        "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.op_Plus_Dot",
        "equation_Lib.IntTypes.op_Star_Bang",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint128", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.l_True",
        "equation_Prims.logical", "equation_Prims.nat", "equation_Prims.pos",
        "equation_Spec.Curve25519.add",
        "equation_Spec.Curve25519.add_and_double",
        "equation_Spec.Curve25519.double", "equation_Spec.Curve25519.elem",
        "equation_Spec.Curve25519.op_Plus_Percent",
        "equation_Spec.Curve25519.op_Subtraction_Percent",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Hacl.Spec.Curve25519.Field51.Definition.lemma_pow_64_51",
        "function_token_typing_Lib.IntTypes.add",
        "function_token_typing_Lib.IntTypes.add_mod",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
        "l_and-interp",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.Buffer.modifies_sub", "lemma_Lib.IntTypes.add_lemma",
        "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mul_lemma",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
        "lemma_LowStar.Monotonic.Buffer.frameOf_gsub",
        "lemma_LowStar.Monotonic.Buffer.gsub_gsub",
        "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
        "lemma_LowStar.Monotonic.Buffer.len_gsub",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.live_gsub",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_l",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_buffer",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_union_comm",
        "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer",
        "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
        "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__5",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
        "refinement_interpretation_Tm_refine_26acdc3a3c64c274ac5624d37abd9647",
        "refinement_interpretation_Tm_refine_303dbbbbac215a323c33becd5402c469",
        "refinement_interpretation_Tm_refine_369d61bb384f6181cd6f792cf86a5d86",
        "refinement_interpretation_Tm_refine_3e7d6cbf9a788b81a5dd3182e0f2ca67",
        "refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
        "refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
        "refinement_interpretation_Tm_refine_57375a59a15fdba9d28699b60620755b",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_6e0752342dfed3b3058e56e9396850f5",
        "refinement_interpretation_Tm_refine_7f12787f8469a0a16508d2424076f15d",
        "refinement_interpretation_Tm_refine_82b65099892bcd4ee1cd969350ddb986",
        "refinement_interpretation_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_Tm_refine_9a274fc908af7df14951b1497176a151",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_9e4fe5e2f1756f97f5c5f41ac37c2845",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_a693852855ed287d59ccdfa545a59688",
        "refinement_interpretation_Tm_refine_abfbc855f1855c1bece906940ccad930",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_b706c37ee15a83b30028d870fb33463b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_cd388606af406d25a6d7024b316ae909",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.add_mod",
        "token_correspondence_Lib.IntTypes.mul",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "token_correspondence_Lib.IntTypes.op_Plus_Dot",
        "token_correspondence_Lib.IntTypes.op_Star_Bang",
        "token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
        "typing_Hacl.Impl.Curve25519.AddAndDouble.get_x",
        "typing_Hacl.Impl.Curve25519.AddAndDouble.get_z",
        "typing_Hacl.Spec.Curve25519.Field51.Definition.max51",
        "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51",
        "typing_Lib.Buffer.gsub", "typing_Lib.Buffer.length",
        "typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar",
        "typing_Lib.Buffer.union", "typing_Lib.IntTypes.add_mod",
        "typing_Lib.IntTypes.op_Plus_Dot",
        "typing_Lib.IntTypes.op_Star_Bang", "typing_Lib.IntTypes.uint_v",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_LowStar.Monotonic.Buffer.mgsub",
        "typing_X64.CPU_Features_s.adx_enabled",
        "typing_X64.CPU_Features_s.bmi2_enabled",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "5f0bbc7c9abf5a45c93e26148420259d"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_add_and_double",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_interpretation_Tm_arrow_3075805bd3b44f3280b499ecd8caf607",
        "Lib.IntTypes_interpretation_Tm_arrow_4b8a7e8fecc07184d556939df4311fa6",
        "Lib.IntTypes_interpretation_Tm_arrow_83846359b5c580ebf2d901d5a0596af0",
        "Lib.IntTypes_interpretation_Tm_arrow_c605800875b6adf350acbdf637102661",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Hacl.Impl.Curve25519.Fields.field_spec__uu___haseq",
        "b2t_def", "bool_inversion", "bool_typing",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point",
        "equation_Hacl.Impl.Curve25519.Fields.felem_wide2",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.gsub",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.op_Plus_Dot",
        "equation_Lib.IntTypes.op_Star_Bang",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Lib.IntTypes.add",
        "function_token_typing_Lib.IntTypes.mul",
        "function_token_typing_Lib.IntTypes.op_Plus_Bang",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma",
        "lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
        "refinement_interpretation_Tm_refine_303dbbbbac215a323c33becd5402c469",
        "refinement_interpretation_Tm_refine_3e7d6cbf9a788b81a5dd3182e0f2ca67",
        "refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_b706c37ee15a83b30028d870fb33463b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.add_mod",
        "token_correspondence_Lib.IntTypes.mul",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "token_correspondence_Lib.IntTypes.op_Plus_Dot",
        "token_correspondence_Lib.IntTypes.op_Star_Bang",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "93934042cfc89941c29577ccdc7f9cac"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_add_and_double",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "c26c7db6be5fcbd0ee8370676edb4063"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_add_and_double",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_interpretation_Tm_arrow_3075805bd3b44f3280b499ecd8caf607",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "disc_equation_Hacl.Impl.Curve25519.Fields.M51",
        "disc_equation_Hacl.Impl.Curve25519.Fields.M64",
        "equality_tok_Hacl.Impl.Curve25519.Fields.M51@tok",
        "equality_tok_Hacl.Impl.Curve25519.Fields.M64@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.get_x",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.get_z",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point",
        "equation_Hacl.Impl.Curve25519.Fields.felem_wide2",
        "equation_Hacl.Impl.Curve25519.Fields.state_inv_t",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.op_Star_Bang",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint128", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.add",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
        "lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.mul_lemma",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
        "refinement_interpretation_Tm_refine_26acdc3a3c64c274ac5624d37abd9647",
        "refinement_interpretation_Tm_refine_3e7d6cbf9a788b81a5dd3182e0f2ca67",
        "refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_6dbba13683db999bf4ed637723558832",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a22934f0046305f91bea274987a97a70",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.mul",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "token_correspondence_Lib.IntTypes.op_Star_Bang",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_FStar.UInt32.v",
        "typing_Hacl.Impl.Curve25519.AddAndDouble.get_x",
        "typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_X64.CPU_Features_s.adx_enabled",
        "typing_X64.CPU_Features_s.bmi2_enabled",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "a7931830ff5930a03afc6f34afb01cc3"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_double_",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Hacl.Impl.Curve25519.Fields.field_spec__uu___haseq",
        "b2t_def", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "3aa7ebc16baa610b3de92059d0e17a6f"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_double_",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "d1a8c72841296738ca05ce6b993a4080"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_double_",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Lib.IntTypes_interpretation_Tm_arrow_49f388450e5cfc91da46292c2a5d5b7b",
        "Lib.IntTypes_interpretation_Tm_arrow_69980de4b69ce434f89b12e4cb716d05",
        "Lib.IntTypes_interpretation_Tm_arrow_78f083cf1c0c989cac96323dae7f10ad",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.SEC",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Hacl.Impl.Curve25519.Fields.M64@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U128@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.fget_x",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.fget_xz",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.fget_z",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.get_x",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.get_z",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point",
        "equation_Hacl.Impl.Curve25519.Field51.as_felem",
        "equation_Hacl.Impl.Curve25519.Field51.as_nat",
        "equation_Hacl.Impl.Curve25519.Field51.felem_fits",
        "equation_Hacl.Impl.Curve25519.Field51.mul_inv_t",
        "equation_Hacl.Impl.Curve25519.Field64.Core.as_nat",
        "equation_Hacl.Impl.Curve25519.Fields.as_nat",
        "equation_Hacl.Impl.Curve25519.Fields.fadd_fsub_pre",
        "equation_Hacl.Impl.Curve25519.Fields.fadd_post",
        "equation_Hacl.Impl.Curve25519.Fields.felem_wide2",
        "equation_Hacl.Impl.Curve25519.Fields.feval",
        "equation_Hacl.Impl.Curve25519.Fields.fmul1_pre",
        "equation_Hacl.Impl.Curve25519.Fields.fmul2_fsqr2_post",
        "equation_Hacl.Impl.Curve25519.Fields.fmul2_pre",
        "equation_Hacl.Impl.Curve25519.Fields.fsqr2_pre",
        "equation_Hacl.Impl.Curve25519.Fields.fsub_post",
        "equation_Hacl.Impl.Curve25519.Fields.state_inv_t",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.max51",
        "equation_Hacl.Spec.Curve25519.Field51.Definition.scale64",
        "equation_Hacl.Spec.Curve25519.Field51.mul_inv_t",
        "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
        "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.gsub",
        "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
        "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
        "equation_Lib.Buffer.modifies",
        "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.op_Plus_Dot",
        "equation_Lib.IntTypes.op_Star_Bang",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint128", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Curve25519.double",
        "equation_Spec.Curve25519.elem",
        "equation_Spec.Curve25519.op_Plus_Percent",
        "equation_Spec.Curve25519.op_Star_Percent",
        "equation_Spec.Curve25519.op_Subtraction_Percent",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Hacl.Spec.Curve25519.Field51.Definition.lemma_pow_64_51",
        "function_token_typing_Lib.IntTypes.add_mod",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "l_and-interp",
        "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.Buffer.modifies_preserves_live",
        "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.add_mod_lemma",
        "lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.pow2_values",
        "lemma_LowStar.Monotonic.Buffer.gsub_gsub",
        "lemma_LowStar.Monotonic.Buffer.length_null_1",
        "lemma_LowStar.Monotonic.Buffer.length_null_2",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
        "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
        "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
        "lemma_LowStar.Monotonic.Buffer.loc_union_comm",
        "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
        "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
        "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__4",
        "projection_inverse_FStar.Pervasives.Native.Mktuple5__5",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
        "refinement_interpretation_Tm_refine_28126c3229332b283e908c1fa6d2bdda",
        "refinement_interpretation_Tm_refine_303dbbbbac215a323c33becd5402c469",
        "refinement_interpretation_Tm_refine_3caca10744a02e94ade352198adc6d62",
        "refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
        "refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
        "refinement_interpretation_Tm_refine_53f0a85cea67593aeb290e09115f43db",
        "refinement_interpretation_Tm_refine_590b8e485b7d51c978dd811a74a85d9e",
        "refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
        "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_6e0752342dfed3b3058e56e9396850f5",
        "refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
        "refinement_interpretation_Tm_refine_7f12787f8469a0a16508d2424076f15d",
        "refinement_interpretation_Tm_refine_82b65099892bcd4ee1cd969350ddb986",
        "refinement_interpretation_Tm_refine_847b35cdbc4d3703552d4865eba7d025",
        "refinement_interpretation_Tm_refine_8af61d0447e6887060c2411d0a533c0b",
        "refinement_interpretation_Tm_refine_9918c305a2eac13fb45cee4b8bcdf9cd",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_a4d846f75d08409fefe20d97e8c8a5cc",
        "refinement_interpretation_Tm_refine_a9a80ef2a511c8fb06ad2cc272062b5e",
        "refinement_interpretation_Tm_refine_abfbc855f1855c1bece906940ccad930",
        "refinement_interpretation_Tm_refine_b2acfbbfcbb392fe00f00ab5af2d0886",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_b706c37ee15a83b30028d870fb33463b",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "refinement_interpretation_Tm_refine_c5f8a6b5af25b27301842abce6ca6c7d",
        "refinement_interpretation_Tm_refine_cc3d2dd476b93d2b20d64200c23c6c04",
        "refinement_interpretation_Tm_refine_e07d49bf7ed472bccb081418af1bddb0",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "refinement_interpretation_Tm_refine_fb1be1d1726d5678dace30d0f3d47eff",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.add_mod",
        "token_correspondence_Lib.IntTypes.mul",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "token_correspondence_Lib.IntTypes.op_Plus_Dot",
        "token_correspondence_Lib.IntTypes.op_Star_Bang",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.add",
        "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
        "typing_Hacl.Impl.Curve25519.AddAndDouble.get_x",
        "typing_Hacl.Impl.Curve25519.AddAndDouble.get_z",
        "typing_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1",
        "typing_Hacl.Spec.Curve25519.Field51.Definition.max51",
        "typing_Hacl.Spec.Curve25519.Field51.Definition.pow51",
        "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.gsub",
        "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
        "typing_Lib.Buffer.op_Bar_Plus_Bar", "typing_Lib.IntTypes.add_mod",
        "typing_Lib.IntTypes.op_Plus_Dot",
        "typing_Lib.IntTypes.op_Star_Bang", "typing_Lib.IntTypes.uint_v",
        "typing_Lib.Sequence.index",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.loc_buffer",
        "typing_LowStar.Monotonic.Buffer.mgsub",
        "typing_X64.CPU_Features_s.adx_enabled",
        "typing_X64.CPU_Features_s.bmi2_enabled",
        "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "7c47de2d2081e3ff86859890f17774f6"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_double_51",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point51",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok"
      ],
      0,
      "aa15cbc367fe78b208c4f644b2e0fda5"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_double_64",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point64",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
        "typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_tok_Lib.Buffer.MUT@tok"
      ],
      0,
      "28beb274b462da224967aa026f2326ce"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_double",
      1,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "assumption_Hacl.Impl.Curve25519.Fields.field_spec__uu___haseq",
        "b2t_def", "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "122154fc2b54dcf412964d573ee8a018"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_double",
      2,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "equation_Prims.pos",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Prims.pow2.fuel_instrumented"
      ],
      0,
      "1e7ac2e83abed95015f57900de7e378f"
    ],
    [
      "Hacl.Impl.Curve25519.AddAndDouble.point_double",
      3,
      1,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
        "constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
        "constructor_distinct_Lib.Buffer.MUT",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "disc_equation_Hacl.Impl.Curve25519.Fields.M51",
        "disc_equation_Hacl.Impl.Curve25519.Fields.M64",
        "equality_tok_Hacl.Impl.Curve25519.Fields.M51@tok",
        "equality_tok_Hacl.Impl.Curve25519.Fields.M64@tok",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.Monotonic.HyperHeap.hmap",
        "equation_FStar.Monotonic.HyperStack.is_tip",
        "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
        "equation_FStar.Monotonic.HyperStack.mem",
        "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.get_x",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.get_z",
        "equation_Hacl.Impl.Curve25519.AddAndDouble.point",
        "equation_Hacl.Impl.Curve25519.Fields.felem_wide2",
        "equation_Hacl.Impl.Curve25519.Fields.state_inv_t",
        "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.op_Plus_Bang",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.uint128", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_LowStar.Buffer.buffer",
        "equation_LowStar.Buffer.trivial_preorder",
        "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
        "fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
        "function_token_typing_FStar.Monotonic.Heap.heap",
        "function_token_typing_Lib.IntTypes.uint128",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.uv_inv",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma",
        "lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
        "refinement_interpretation_Tm_refine_31853c033fec99a90d30a5eb7b521a25",
        "refinement_interpretation_Tm_refine_970b98cafcb988cbe0a9f11af17f3c85",
        "refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b2acfbbfcbb392fe00f00ab5af2d0886",
        "refinement_interpretation_Tm_refine_b44adca49ccd6a8727e23d566a34e43f",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
        "token_correspondence_Lib.IntTypes.add",
        "token_correspondence_Lib.IntTypes.op_Plus_Bang",
        "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
        "typing_FStar.Monotonic.HyperStack.get_hmap",
        "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v",
        "typing_Hacl.Impl.Curve25519.AddAndDouble.get_x",
        "typing_LowStar.Buffer.trivial_preorder",
        "typing_LowStar.Monotonic.Buffer.len",
        "typing_X64.CPU_Features_s.adx_enabled",
        "typing_X64.CPU_Features_s.bmi2_enabled",
        "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "511b72b73dc2e8503629b5a8fd544a6f"
    ]
  ]
]