Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC
OCaml API: Don't run unit tests which require unsupported features
Hacl.Spec.Curve25519.Field64.Core.fst.hints
[
"�r�)kC\u0011�=\u000e\u001a�\rnV",
[
[
"Hacl.Spec.Curve25519.Field64.Core.addcarry",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.lt",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt64.lt",
"equation_Hacl.Spec.Curve25519.Field64.Core.lt_u64",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma",
"lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Addition",
"primitive_Prims.op_LessThan", "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",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_a6fce85b67bdd71ab9416e435ac3b18a",
"refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e",
"refinement_interpretation_Tm_refine_cde1a45129380071fe620b72e00a03d7",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt64.v", "typing_Lib.IntTypes.add_mod",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.maxint",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.sec_int_v",
"typing_Lib.IntTypes.v", "typing_Lib.RawIntTypes.u64_to_UInt64",
"typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"a3a0862aa3e659b53799bd3c1339d4b6"
],
[
"Hacl.Spec.Curve25519.Field64.Core.subborrow",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.eq",
"equation_FStar.UInt.lt", "equation_FStar.UInt.lte",
"equation_FStar.UInt.max_int", "equation_FStar.UInt64.eq",
"equation_FStar.UInt64.lt", "equation_FStar.UInt64.lte",
"equation_Hacl.Spec.Curve25519.Field64.Core.eq_u64",
"equation_Hacl.Spec.Curve25519.Field64.Core.le_u64",
"equation_Hacl.Spec.Curve25519.Field64.Core.lt_u64",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.sub_mod_lemma", "lemma_Lib.IntTypes.v_injective",
"primitive_Prims.op_Equality", "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",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a6fce85b67bdd71ab9416e435ac3b18a",
"refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e",
"refinement_interpretation_Tm_refine_cde1a45129380071fe620b72e00a03d7",
"refinement_interpretation_Tm_refine_f41f4015e22b272c5f61be9cc1570311",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.op_At_Percent_Dot",
"typing_Lib.IntTypes.v", "typing_Lib.RawIntTypes.u64_to_UInt64",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"2c9b22f6e37228bfe50599164fe0c1d6"
],
[
"Hacl.Spec.Curve25519.Field64.Core.mul64",
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.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"disc_equation_Lib.IntTypes.SEC",
"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.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.mul64_wide_lemma",
"lemma_Lib.IntTypes.pow2_127",
"lemma_Lib.IntTypes.shift_right_lemma",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "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",
"refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
"refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7",
"refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt32.uint_to_t", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.cast", "typing_Lib.IntTypes.v",
"typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"3ba1059fd2e6f8acf45c3f2510be6e95"
],
[
"Hacl.Spec.Curve25519.Field64.Core.add0carry",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.lt", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt64.lt",
"equation_Hacl.Spec.Curve25519.Field64.Core.lt_u64",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma",
"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",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a6fce85b67bdd71ab9416e435ac3b18a",
"refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e",
"refinement_interpretation_Tm_refine_cde1a45129380071fe620b72e00a03d7",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt64.v", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.v", "typing_Lib.RawIntTypes.u64_to_UInt64",
"typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"51fcbd793666ffd1af7629e6328752ae"
],
[
"Hacl.Spec.Curve25519.Field64.Core.add1",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.lt", "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.lt_u64",
"equation_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.v_injective",
"lemma_Lib.IntTypes.v_mk_int",
"lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThan", "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_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_d9aa70e8ea65546e86a9449fdf12b243",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt64.v", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v",
"typing_Lib.RawIntTypes.u64_to_UInt64", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"11ceb742f45ddade18af2ef20bdb7f37"
],
[
"Hacl.Spec.Curve25519.Field64.Core.sub1",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U64",
"data_typing_intro_FStar.Pervasives.Native.Mktuple4@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.eq",
"equation_FStar.UInt.fits", "equation_FStar.UInt.lt",
"equation_FStar.UInt.lte", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt64.eq", "equation_FStar.UInt64.lt",
"equation_FStar.UInt64.lte",
"equation_Hacl.Spec.Curve25519.Field64.Core.eq_u64",
"equation_Hacl.Spec.Curve25519.Field64.Core.le_u64",
"equation_Hacl.Spec.Curve25519.Field64.Core.lt_u64",
"equation_Hacl.Spec.Curve25519.Field64.Core.subborrow",
"equation_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Lib.IntTypes.uint64", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt64.uv_inv", "lemma_Lib.IntTypes.sub_mod_lemma",
"lemma_Lib.IntTypes.v_injective",
"lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "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_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e",
"refinement_interpretation_Tm_refine_d9aa70e8ea65546e86a9449fdf12b243",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.UInt64.v",
"typing_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.sub_mod", "typing_Lib.IntTypes.v",
"typing_Lib.RawIntTypes.u64_to_UInt64", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"8d229b99e3aa78f4bab8c611768a4dab"
],
[
"Hacl.Spec.Curve25519.Field64.Core.mul1",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U64",
"data_typing_intro_FStar.Pervasives.Native.Mktuple4@tok",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U128@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.lt", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt64.lt",
"equation_Hacl.Spec.Curve25519.Field64.Core.addcarry",
"equation_Hacl.Spec.Curve25519.Field64.Core.lt_u64",
"equation_Hacl.Spec.Curve25519.Field64.Core.mul64",
"equation_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Lib.IntTypes.uint64", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.add_mod_lemma",
"lemma_Lib.IntTypes.mul64_wide_lemma",
"lemma_Lib.IntTypes.v_injective",
"lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
"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.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_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7",
"refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_a6fce85b67bdd71ab9416e435ac3b18a",
"refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.UInt.fits", "typing_FStar.UInt64.v",
"typing_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
"typing_Lib.IntTypes.add_mod", "typing_Lib.IntTypes.cast",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.mul64_wide",
"typing_Lib.IntTypes.v", "typing_Lib.RawIntTypes.u64_to_UInt64",
"typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"333fff81e10cdea22eb231f5b92e8c74"
],
[
"Hacl.Spec.Curve25519.Field64.Core.mul1_add",
1,
2,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.U64",
"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.felem4",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_Lib.IntTypes.add_lemma",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e",
"refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a",
"typing_Lib.IntTypes.v", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"8b22b49e4004606c0d85d5a8a5c206aa"
],
[
"Hacl.Spec.Curve25519.Field64.Core.carry_pass",
1,
2,
1,
[ "@query" ],
0,
"09170aa7917246b5940479e8f22014f6"
],
[
"Hacl.Spec.Curve25519.Field64.Core.carry_pass",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.U64",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_FStar.Pervasives.Native.Mktuple4",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.lt", "equation_FStar.UInt.max_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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Curve25519.prime",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple4",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.mul_lemma",
"lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int",
"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_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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_ab07f5311d61184bc6075f362eefa7d3",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_caca8ead99c687280eab655af2625a10",
"refinement_interpretation_Tm_refine_d113499eb2f48e1a5a1fe6208e65e6bc",
"refinement_interpretation_Tm_refine_d9aa70e8ea65546e86a9449fdf12b243",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a",
"typing_FStar.UInt.fits", "typing_FStar.UInt64.v",
"typing_Hacl.Spec.Curve25519.Field64.Core.add0carry",
"typing_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
"typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.v", "typing_Lib.RawIntTypes.u64_to_UInt64",
"typing_Spec.Curve25519.prime", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"6cf845eae084049043315de6548783c3"
],
[
"Hacl.Spec.Curve25519.Field64.Core.carry_wide",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.U64",
"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.felem4",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_4",
"lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_caca8ead99c687280eab655af2625a10",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"21fbabca653f836e12f546873099782d"
],
[
"Hacl.Spec.Curve25519.Field64.Core.add4",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.pos", "int_typing",
"lemma_FStar.UInt.pow2_values",
"lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
"typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"e76ed8313068cd3dda6033510e6ff965"
],
[
"Hacl.Spec.Curve25519.Field64.Core.fadd4",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.feval",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.Curve25519.fadd",
"equation_Spec.Curve25519.prime",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple4",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_aa1f30dab2624caf19ab06fe1a881d01",
"typing_Spec.Curve25519.prime"
],
0,
"848dd3475c81589f54c75a79a9a085cc"
],
[
"Hacl.Spec.Curve25519.Field64.Core.sub4",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.eq",
"equation_FStar.UInt64.eq",
"equation_Hacl.Spec.Curve25519.Field64.Core.eq_u64",
"equation_Hacl.Spec.Curve25519.Field64.Core.subborrow",
"equation_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.v_injective",
"lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e",
"refinement_interpretation_Tm_refine_d9aa70e8ea65546e86a9449fdf12b243",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.v", "typing_Lib.RawIntTypes.u64_to_UInt64",
"typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"1a1f1a8194a5a1e44339feb8b4c57e9c"
],
[
"Hacl.Spec.Curve25519.Field64.Core.fsub4",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"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",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.eq",
"equation_FStar.UInt.fits", "equation_FStar.UInt.lt",
"equation_FStar.UInt.lte", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt64.eq", "equation_FStar.UInt64.lt",
"equation_FStar.UInt64.lte",
"equation_Hacl.Spec.Curve25519.Field64.Core.eq_u64",
"equation_Hacl.Spec.Curve25519.Field64.Core.le_u64",
"equation_Hacl.Spec.Curve25519.Field64.Core.lt_u64",
"equation_Hacl.Spec.Curve25519.Field64.Core.sub1",
"equation_Hacl.Spec.Curve25519.Field64.Core.sub4",
"equation_Hacl.Spec.Curve25519.Field64.Core.subborrow",
"equation_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.feval",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple4",
"function_token_typing_Lib.IntTypes.uint64", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt64.uv_inv", "lemma_Lib.IntTypes.mul_lemma",
"lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.v_injective",
"lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual", "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_1cc58e901e83e96dff5b4d1682343605",
"refinement_interpretation_Tm_refine_4fcd12e6783f9f96af8c0be135f611a6",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a6fce85b67bdd71ab9416e435ac3b18a",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_caca8ead99c687280eab655af2625a10",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f41f4015e22b272c5f61be9cc1570311",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.UInt.fits", "typing_FStar.UInt64.v",
"typing_Hacl.Spec.Curve25519.Field64.Core.subborrow",
"typing_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
"typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.v", "typing_Lib.RawIntTypes.u64_to_UInt64",
"typing_Prims.pow2", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"b82f75a8e677124e659a4d63b5bada40"
],
[
"Hacl.Spec.Curve25519.Field64.Core.mul4",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U64",
"data_elim_FStar.Pervasives.Native.Mktuple4",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U128@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Hacl.Spec.Curve25519.Field64.Core.addcarry",
"equation_Hacl.Spec.Curve25519.Field64.Core.mul1",
"equation_Hacl.Spec.Curve25519.Field64.Core.mul64",
"equation_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.wide_as_nat4",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple4",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.mul64_wide_lemma", "primitive_Prims.op_Addition",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7",
"refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_d9aa70e8ea65546e86a9449fdf12b243",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt64.v",
"typing_Lib.IntTypes.cast", "typing_Lib.IntTypes.mul64_wide",
"typing_Lib.IntTypes.v", "typing_Lib.RawIntTypes.u64_to_UInt64",
"typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U128@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"31ada2115c771a2d6afd104653ed4650"
],
[
"Hacl.Spec.Curve25519.Field64.Core.fmul4",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Curve25519.Field64.Core.mul4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.feval",
"equation_Hacl.Spec.Curve25519.Field64.Definition.feval_wide",
"equation_Lib.IntTypes.uint64", "equation_Prims.pos",
"equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.prime",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple4",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8e5d4912c82b9576bb620db91a9a2821",
"typing_Hacl.Spec.Curve25519.Field64.Core.mul4",
"typing_Spec.Curve25519.prime"
],
0,
"49c41b6ccc0b563f1936cdf8f3881a55"
],
[
"Hacl.Spec.Curve25519.Field64.Core.fmul14",
1,
2,
1,
[ "@query" ],
0,
"297cb97383736df6a007b55477e03de0"
],
[
"Hacl.Spec.Curve25519.Field64.Core.fmul14",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Hacl.Spec.Curve25519.Field64.Core.mul1",
"equation_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.feval",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Curve25519.prime",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple4",
"int_typing", "lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_1d67f7edd169c14b803c1b2963a4f093",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_aa1f30dab2624caf19ab06fe1a881d01",
"typing_Hacl.Spec.Curve25519.Field64.Definition.as_nat4",
"typing_Lib.IntTypes.v", "typing_Spec.Curve25519.prime",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"7d397ca6008cf25c3dc987141e874a0c"
],
[
"Hacl.Spec.Curve25519.Field64.Core.fsqr4",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Curve25519.Field64.Core.sqr4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.felem4",
"equation_Hacl.Spec.Curve25519.Field64.Definition.feval",
"equation_Hacl.Spec.Curve25519.Field64.Definition.feval_wide",
"equation_Lib.IntTypes.uint64", "equation_Prims.pos",
"equation_Spec.Curve25519.fmul", "equation_Spec.Curve25519.prime",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple4",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8e5d4912c82b9576bb620db91a9a2821",
"typing_Hacl.Spec.Curve25519.Field64.Core.mul4",
"typing_Spec.Curve25519.prime"
],
0,
"81d0168642b63536530af320057c477a"
]
]
]
Computing file changes ...
