[
  "�է�q���\u0016jnBD",
  [
    [
      "Hacl.Spec.Curve25519.Field64.carry_pass_store",
      1,
      2,
      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",
        "constructor_distinct_Lib.IntTypes.U64",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U64@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_Greater_Greater_Dot",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64",
        "equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Prims.__cache_version_number__", "int_typing",
        "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
        "lemma_Lib.IntTypes.shift_right_lemma", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "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_2089d4dca730bb398d9189361fbc0b15",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_92eedd657384b0981bcfc64b33308eaf",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "token_correspondence_Lib.IntTypes.op_Greater_Greater_Dot",
        "token_correspondence_Lib.IntTypes.shift_right",
        "typing_FStar.UInt32.uint_to_t", "typing_Lib.IntTypes.uint_v",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "6f13fa35dfd9fdd86fecb1d0f4bd6929"
    ],
    [
      "Hacl.Spec.Curve25519.Field64.lemma_carry_pass_store0",
      1,
      2,
      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",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "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.UInt.fits",
        "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt64.lt",
        "equation_Hacl.Spec.Curve25519.Field64.Core.add0carry",
        "equation_Hacl.Spec.Curve25519.Field64.Core.add1",
        "equation_Hacl.Spec.Curve25519.Field64.Core.lt_u64",
        "equation_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
        "equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
        "equation_Hacl.Spec.Curve25519.Field64.Definition.feval",
        "equation_Hacl.Spec.Curve25519.Field64.carry_pass_store",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.mod_mask",
        "equation_Lib.IntTypes.op_Amp_Dot",
        "equation_Lib.IntTypes.op_Greater_Greater_Dot",
        "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.shiftval", "equation_Lib.IntTypes.u64",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Curve25519.prime",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Lib.IntTypes.add_mod",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mul_lemma",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_Lib.IntTypes.shift_left_lemma",
        "lemma_Lib.IntTypes.shift_right_lemma",
        "lemma_Lib.IntTypes.sub_mod_lemma",
        "lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
        "lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "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.Mktuple4__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__4",
        "refinement_interpretation_Tm_refine_2089d4dca730bb398d9189361fbc0b15",
        "refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
        "refinement_interpretation_Tm_refine_256bb619b0dcc9559ae915e324c2d0b9",
        "refinement_interpretation_Tm_refine_2fc46574a4475201c503d26411f582a8",
        "refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
        "refinement_interpretation_Tm_refine_578bf3235578684f25c2e63d5cb4ac61",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_847e96a1feedc748e1951d8c6bc1015e",
        "refinement_interpretation_Tm_refine_92eedd657384b0981bcfc64b33308eaf",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c67cd54e2afeccac2b00fa9aa3a15ab1",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Lib.IntTypes.add_mod",
        "token_correspondence_Lib.IntTypes.logand",
        "token_correspondence_Lib.IntTypes.mul",
        "token_correspondence_Lib.IntTypes.op_Amp_Dot",
        "token_correspondence_Lib.IntTypes.op_Greater_Greater_Dot",
        "token_correspondence_Lib.IntTypes.op_Plus_Dot",
        "token_correspondence_Lib.IntTypes.op_Star_Bang",
        "token_correspondence_Lib.IntTypes.shift_right",
        "typing_FStar.UInt32.uint_to_t",
        "typing_Hacl.Spec.Curve25519.Field64.Core.add0carry",
        "typing_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
        "typing_Lib.IntTypes.nat_to_uint", "typing_Lib.IntTypes.shift_left",
        "typing_Lib.IntTypes.u64", "typing_Lib.IntTypes.uint",
        "typing_Lib.IntTypes.uint_v", "typing_Lib.RawIntTypes.u64_to_UInt64",
        "typing_Prims.pow2", "typing_tok_Lib.IntTypes.PUB@tok",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "85e8dbe742983c5c56a5d6fb29b4cd78"
    ],
    [
      "Hacl.Spec.Curve25519.Field64.lemma_carry_pass_store1_0",
      1,
      2,
      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_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U64",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "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.UInt.fits",
        "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt64.lt",
        "equation_Hacl.Spec.Curve25519.Field64.Core.add0carry",
        "equation_Hacl.Spec.Curve25519.Field64.Core.add1",
        "equation_Hacl.Spec.Curve25519.Field64.Core.lt_u64",
        "equation_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
        "equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
        "equation_Hacl.Spec.Curve25519.Field64.Definition.feval",
        "equation_Hacl.Spec.Curve25519.Field64.carry_pass_store",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.mod_mask",
        "equation_Lib.IntTypes.op_Amp_Dot",
        "equation_Lib.IntTypes.op_Greater_Greater_Dot",
        "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.shiftval", "equation_Lib.IntTypes.u64",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "equation_Prims.pos",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Lib.IntTypes.add_mod",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt32.vu_inv",
        "lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mul_lemma",
        "lemma_Lib.IntTypes.pow2_values",
        "lemma_Lib.IntTypes.shift_left_lemma",
        "lemma_Lib.IntTypes.shift_right_lemma",
        "lemma_Lib.IntTypes.sub_mod_lemma",
        "lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
        "lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "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.Mktuple4__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__4",
        "refinement_interpretation_Tm_refine_2089d4dca730bb398d9189361fbc0b15",
        "refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
        "refinement_interpretation_Tm_refine_256bb619b0dcc9559ae915e324c2d0b9",
        "refinement_interpretation_Tm_refine_2fc46574a4475201c503d26411f582a8",
        "refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
        "refinement_interpretation_Tm_refine_578bf3235578684f25c2e63d5cb4ac61",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_847e96a1feedc748e1951d8c6bc1015e",
        "refinement_interpretation_Tm_refine_92eedd657384b0981bcfc64b33308eaf",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c67cd54e2afeccac2b00fa9aa3a15ab1",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Lib.IntTypes.add_mod",
        "token_correspondence_Lib.IntTypes.logand",
        "token_correspondence_Lib.IntTypes.mul",
        "token_correspondence_Lib.IntTypes.op_Amp_Dot",
        "token_correspondence_Lib.IntTypes.op_Greater_Greater_Dot",
        "token_correspondence_Lib.IntTypes.op_Plus_Dot",
        "token_correspondence_Lib.IntTypes.op_Star_Bang",
        "token_correspondence_Lib.IntTypes.shift_right",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_Hacl.Spec.Curve25519.Field64.Core.add0carry",
        "typing_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
        "typing_Lib.IntTypes.nat_to_uint", "typing_Lib.IntTypes.shift_left",
        "typing_Lib.IntTypes.u64", "typing_Lib.IntTypes.uint",
        "typing_Lib.IntTypes.uint_v", "typing_Lib.RawIntTypes.u64_to_UInt64",
        "typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "1f78d59dc814fa0bafe35c45d556e88c"
    ],
    [
      "Hacl.Spec.Curve25519.Field64.lemma_carry_pass_store1_1",
      1,
      2,
      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_64d9bcf6dc13bcbde626455717781a82",
        "Lib.IntTypes_interpretation_Tm_arrow_69980de4b69ce434f89b12e4cb716d05",
        "Lib.IntTypes_interpretation_Tm_arrow_83846359b5c580ebf2d901d5a0596af0",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "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",
        "data_elim_FStar.Pervasives.Native.Mktuple2",
        "data_elim_FStar.Pervasives.Native.Mktuple4",
        "data_typing_intro_FStar.Pervasives.Native.Mktuple4@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.UInt.fits",
        "equation_FStar.UInt.lt", "equation_FStar.UInt.max_int",
        "equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
        "equation_FStar.UInt.uint_t", "equation_FStar.UInt64.lt",
        "equation_Hacl.Spec.Curve25519.Field64.Core.add0carry",
        "equation_Hacl.Spec.Curve25519.Field64.Core.add1",
        "equation_Hacl.Spec.Curve25519.Field64.Core.lt_u64",
        "equation_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
        "equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
        "equation_Hacl.Spec.Curve25519.Field64.Definition.feval",
        "equation_Hacl.Spec.Curve25519.Field64.carry_pass_store",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.mod_mask",
        "equation_Lib.IntTypes.op_Amp_Dot",
        "equation_Lib.IntTypes.op_Greater_Greater_Dot",
        "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.shiftval", "equation_Lib.IntTypes.u64",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
        "equation_Lib.IntTypes.uint_v", "equation_Prims.nat",
        "equation_Prims.pos", "equation_Spec.Curve25519.prime",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Lib.IntTypes.add_mod",
        "function_token_typing_Lib.IntTypes.mul",
        "function_token_typing_Lib.IntTypes.op_Plus_Dot",
        "function_token_typing_Lib.IntTypes.uint64",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing", "lemma_FStar.UInt32.vu_inv",
        "lemma_FStar.UInt64.uv_inv", "lemma_Lib.IntTypes.add_mod_lemma",
        "lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.pow2_values",
        "lemma_Lib.IntTypes.shift_left_lemma",
        "lemma_Lib.IntTypes.shift_right_lemma",
        "lemma_Lib.IntTypes.sub_mod_lemma",
        "lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
        "lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_Division", "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.Mktuple4__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__4",
        "refinement_interpretation_Tm_refine_2089d4dca730bb398d9189361fbc0b15",
        "refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
        "refinement_interpretation_Tm_refine_256bb619b0dcc9559ae915e324c2d0b9",
        "refinement_interpretation_Tm_refine_2fc46574a4475201c503d26411f582a8",
        "refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
        "refinement_interpretation_Tm_refine_578bf3235578684f25c2e63d5cb4ac61",
        "refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
        "refinement_interpretation_Tm_refine_847e96a1feedc748e1951d8c6bc1015e",
        "refinement_interpretation_Tm_refine_92eedd657384b0981bcfc64b33308eaf",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
        "refinement_interpretation_Tm_refine_b706c37ee15a83b30028d870fb33463b",
        "refinement_interpretation_Tm_refine_b7d90ad39ccb3163fe86b9001f583457",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_c67cd54e2afeccac2b00fa9aa3a15ab1",
        "refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
        "refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
        "token_correspondence_Lib.IntTypes.add_mod",
        "token_correspondence_Lib.IntTypes.logand",
        "token_correspondence_Lib.IntTypes.mul",
        "token_correspondence_Lib.IntTypes.op_Amp_Dot",
        "token_correspondence_Lib.IntTypes.op_Greater_Greater_Dot",
        "token_correspondence_Lib.IntTypes.op_Plus_Dot",
        "token_correspondence_Lib.IntTypes.op_Star_Bang",
        "token_correspondence_Lib.IntTypes.shift_right",
        "token_correspondence_Prims.pow2.fuel_instrumented",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_Hacl.Spec.Curve25519.Field64.Core.add0carry",
        "typing_Hacl.Spec.Curve25519.Field64.Core.add1",
        "typing_Hacl.Spec.Curve25519.Field64.carry_pass_store",
        "typing_Lib.IntTypes.nat_to_uint", "typing_Lib.IntTypes.sec_int_v",
        "typing_Lib.IntTypes.shift_left", "typing_Lib.IntTypes.u64",
        "typing_Lib.IntTypes.uint", "typing_Lib.IntTypes.uint_v",
        "typing_Lib.RawIntTypes.u64_to_UInt64", "typing_Prims.pow2",
        "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "0b81a417860d01897f5f116c55f4b483"
    ],
    [
      "Hacl.Spec.Curve25519.Field64.lemma_carry_pass_store1",
      1,
      2,
      1,
      [
        "@query", "equation_Lib.IntTypes.uint64",
        "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__4"
      ],
      0,
      "73c7c331276b38cc25069c605da709b1"
    ],
    [
      "Hacl.Spec.Curve25519.Field64.subtract_p4",
      1,
      2,
      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",
        "constructor_distinct_Lib.IntTypes.U64",
        "disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
        "equality_tok_Lib.IntTypes.U64@tok",
        "equation_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
        "equation_Hacl.Spec.Curve25519.Field64.Definition.feval",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.op_Amp_Dot",
        "equation_Lib.IntTypes.op_Subtraction_Dot",
        "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_v",
        "equation_Prims.nat", "equation_Spec.Curve25519.prime",
        "equation_with_fuel_Prims.pow2.fuel_instrumented",
        "function_token_typing_Lib.IntTypes.logand",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "int_typing",
        "lemma_Lib.IntTypes.eq_mask_logand_lemma",
        "lemma_Lib.IntTypes.gte_mask_lemma",
        "lemma_Lib.IntTypes.pow2_values", "lemma_Lib.IntTypes.sub_mod_lemma",
        "lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
        "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
        "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
        "primitive_Prims.op_GreaterThanOrEqual",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "primitive_Prims.op_disEquality",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__1",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__2",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__3",
        "projection_inverse_FStar.Pervasives.Native.Mktuple4__4",
        "refinement_interpretation_Tm_refine_2fc46574a4475201c503d26411f582a8",
        "refinement_interpretation_Tm_refine_37f52cddf8dfe80174333ac10d59e4cc",
        "refinement_interpretation_Tm_refine_4d2a123888c1d0f0ae91d484f0fe5696",
        "refinement_interpretation_Tm_refine_70769f76f84273b3587aeaec18364fbc",
        "refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "token_correspondence_Lib.IntTypes.logand",
        "token_correspondence_Lib.IntTypes.op_Amp_Dot",
        "token_correspondence_Lib.IntTypes.op_Subtraction_Dot",
        "token_correspondence_Lib.IntTypes.sub_mod",
        "typing_Lib.IntTypes.uint_v", "typing_tok_Lib.IntTypes.SEC@tok",
        "typing_tok_Lib.IntTypes.U64@tok"
      ],
      0,
      "959c614087a98f1ee66322c66208ee35"
    ]
  ]
]