https://github.com/project-everest/hacl-star
Tip revision: 492973e7cf3e9b0c13a36aa776d984d1deae0516 authored by Jonathan Protzenko on 09 March 2018, 21:57:53 UTC
Makefile fixes + support for -fnostruct-passing
Makefile fixes + support for -fnostruct-passing
Tip revision: 492973e
Hacl.Spec.EC.Format.fst.hints
[
"�;#Y���**\u0007�0�\u0018",
[
[
"Hacl.Spec.EC.Format.point_inf",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.point_inf",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.point_inf",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.Mul.op_Star",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt64.n",
"equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t",
"equation_FStar.UInt8.n", "equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n", "equation_Hacl.Bignum.Limb.t",
"equation_Hacl.Bignum.Limb.v", "equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.limb_one",
"equation_Hacl.Bignum.Parameters.limb_zero",
"equation_Hacl.Bignum.Parameters.prime",
"equation_Hacl.Bignum.Parameters.seqelem",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.Field.elem",
"equation_Hacl.Spec.Bignum.Field.one",
"equation_Hacl.Spec.Bignum.selem",
"equation_Hacl.Spec.EC.AddAndDouble.bounds",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.AddAndDouble.p513",
"equation_Hacl.Spec.EC.AddAndDouble.red_513", "equation_Prims.nat",
"equation_Prims.pos", "function_token_typing_FStar.UInt8.n",
"function_token_typing_Hacl.Bignum.Constants.len",
"function_token_typing_Hacl.Bignum.Parameters.limb_one",
"function_token_typing_Hacl.Bignum.Parameters.limb_zero",
"function_token_typing_Hacl.Spec.Bignum.Field.one",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"int_inversion", "int_typing", "kinding_FStar.UInt64.t_@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Base.lemma_len_upd",
"lemma_Hacl.Bignum.Parameters.lemma_limb_injectivity",
"lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"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_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_72320aff465f8f5be1a60f01274a9fe3",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_b6cddb0925a26b22bc7c5884d275beb2",
"refinement_interpretation_Hacl.Spec.Bignum.Field_Tm_refine_64fde586cd61a9af199b0a72fdba45d1",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Hacl.Bignum.Limb.v", "typing_Hacl.Spec.Bignum.Bigint.seval"
],
0
],
[
"Hacl.Spec.EC.Format.point_inf",
4,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.point_inf",
5,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.alloc_point",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.alloc_point",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.alloc_point",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.Mul.op_Star",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt64.n",
"equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t",
"equation_FStar.UInt8.n", "equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n", "equation_Hacl.Bignum.Limb.t",
"equation_Hacl.Bignum.Limb.v", "equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.limb_zero",
"equation_Hacl.Bignum.Parameters.prime",
"equation_Hacl.Bignum.Parameters.seqelem",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.selem",
"equation_Hacl.Spec.EC.AddAndDouble.bounds",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.AddAndDouble.p513",
"equation_Hacl.Spec.EC.AddAndDouble.red_513", "equation_Prims.nat",
"equation_Prims.pos", "function_token_typing_FStar.UInt8.n",
"function_token_typing_Hacl.Bignum.Constants.len",
"function_token_typing_Hacl.Bignum.Parameters.limb_zero",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"int_inversion", "int_typing", "kinding_FStar.UInt64.t_@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"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_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_72320aff465f8f5be1a60f01274a9fe3",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.index", "typing_Hacl.Bignum.Limb.v"
],
0
],
[
"Hacl.Spec.EC.Format.load64_le_spec",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.load64_le_spec",
2,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"haseqHacl.Spec.EC.Format_Tm_refine_530be526726c3b66223dd819f9d65058",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.load64_le_spec",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"equation_FStar.Mul.op_Star", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt64.n", "equation_FStar.UInt8.n",
"equation_FStar.UInt8.t", "equation_FStar.UInt8.uint_to_t",
"equation_FStar.UInt8.v", "equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.v",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Cast.uint8_to_sint8",
"equation_Hacl.Spec.EC.Format.uint8_s",
"equation_Hacl.Spec.EC.Format.zero_8", "equation_Prims.nat",
"function_token_typing_Hacl.Spec.EC.Format.zero_8", "int_typing",
"kinding_FStar.UInt8.t_@tok", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt8.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt8.Mk_v",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_32c347ca7b56982577c8b5684ed24a3c",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_85e39ae6a1ee4b5850e80667b5a19685",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
"typing_FStar.UInt8.v"
],
0
],
[
"Hacl.Spec.EC.Format.store64_le_spec",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.store64_le_spec",
2,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"haseqHacl.Spec.Endianness_Tm_refine_f2c63b31fd0059912139424a133143ce",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.store64_le_spec",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"data_elim_FStar.UInt64.Mk", "equation_FStar.Endianness.bytes",
"equation_FStar.Endianness.lbytes", "equation_FStar.Mul.op_Star",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.uint_to_t",
"equation_FStar.UInt32.v", "equation_FStar.UInt64.n",
"equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
"equation_FStar.UInt8.t", "equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n", "equation_Hacl.Bignum.Limb.t",
"equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.v",
"equation_Hacl.Bignum.Parameters.word_size",
"fuel_guarded_inversion_FStar.UInt64.t_", "int_inversion",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt32.Mk_v",
"refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_c101821d6fd3dd5dd995597323cfbedb"
],
0
],
[
"Hacl.Spec.EC.Format.mask_51",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.mask_51",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.mask_51",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt64.t",
"equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.uint64_to_limb",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.Fsquare.p64",
"equation_Hacl.Spec.Bignum.Modulo.mask_51", "equation_Prims.pos",
"function_token_typing_Hacl.Spec.Bignum.Fsquare.p64",
"function_token_typing_Hacl.Spec.Bignum.Modulo.mask_51",
"proj_equation_FStar.UInt64.Mk_v",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt64.Mk_v",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_da98c95d2af35788da839c6c05bdbc1c",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_ebf171ea18a7d062213a1b4483bc8ed1"
],
0
],
[
"Hacl.Spec.EC.Format.seq_upd_5",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt64.t",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.seqelem",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
],
0
],
[
"Hacl.Spec.EC.Format.seq_upd_5",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query", "data_elim_FStar.UInt32.Mk",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
"equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Parameters.clen",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_one",
"equation_Hacl.Bignum.Parameters.limb_zero",
"equation_Hacl.Cast.uint64_to_sint64", "equation_Prims.nat",
"fuel_guarded_inversion_FStar.UInt64.t_",
"function_token_typing_Hacl.Bignum.Constants.len",
"function_token_typing_Hacl.Bignum.Parameters.clen",
"function_token_typing_Hacl.Bignum.Parameters.limb_one",
"function_token_typing_Hacl.Bignum.Parameters.limb_zero",
"int_typing", "kinding_FStar.UInt64.t_@tok",
"lemma_FStar.Buffer.lemma_size",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_upd",
"lemma_Hacl.Bignum.Parameters.lemma_limb_injectivity",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
"refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_72320aff465f8f5be1a60f01274a9fe3",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_b6cddb0925a26b22bc7c5884d275beb2",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Hacl.Spec.EC.Format.fexpand_spec",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fexpand_spec",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fexpand_spec",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.EC.AddAndDouble.p51", "equation_Prims.pos",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2"
],
0
],
[
"Hacl.Spec.EC.Format.fexpand_spec",
4,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
"equation_FStar.UInt32.v", "equation_FStar.UInt64.logand",
"equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_right",
"equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t",
"equation_FStar.UInt64.v", "equation_FStar.UInt8.n",
"equation_FStar.UInt8.t", "equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.logand", "equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Limb.op_Amp_Hat",
"equation_Hacl.Bignum.Limb.op_Greater_Greater_Hat",
"equation_Hacl.Bignum.Limb.shift_right",
"equation_Hacl.Bignum.Limb.t", "equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_logand",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.limb_one",
"equation_Hacl.Bignum.Parameters.limb_shift_right",
"equation_Hacl.Bignum.Parameters.uint64_to_limb",
"equation_Hacl.Bignum.Parameters.v",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.Modulo.mask_51",
"equation_Hacl.Spec.EC.AddAndDouble.bounds",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.AddAndDouble.p513",
"equation_Hacl.Spec.EC.AddAndDouble.red_513",
"equation_Hacl.Spec.EC.Format.load64_le_spec",
"equation_Hacl.Spec.EC.Format.mask_51",
"equation_Hacl.Spec.EC.Format.seq_upd_5",
"equation_Hacl.Spec.EC.Format.uint8_s", "equation_Prims.nat",
"equation_Prims.pos", "function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt64.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_Hacl.Bignum.Parameters.limb_one",
"function_token_typing_Hacl.Spec.Bignum.Modulo.mask_51",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"function_token_typing_Hacl.Spec.EC.Format.mask_51", "int_typing",
"kinding_FStar.UInt8.t_@tok", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt.shift_right_value_lemma",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
"proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt32.Mk_v",
"projection_inverse_FStar.UInt64.Mk_v",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Limb_Tm_refine_845cb29d79804b7343fe68ed179f6a21",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_af3a13b4eecac03b78c491f7ef2b46d1",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_b6cddb0925a26b22bc7c5884d275beb2",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_ebf171ea18a7d062213a1b4483bc8ed1",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_0957416e4227d4c2de7ea31c497560ef",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_6c25888ad5d42756375005cff93d516d",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_722403efc589333984453beb4c150f71",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_8274173e0780491dcfd7be1a7e81e7bb",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_92f7269f34e25a641d75421bfc43364f",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_bb0eb95c9bf1cf0d7a960b13b49c62a0",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_f26ed7123f8b8bbfb9e0a624ef25680d",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt32.uint_to_t",
"typing_Hacl.Bignum.Limb.op_Greater_Greater_Hat",
"typing_Hacl.Bignum.Limb.v",
"typing_Hacl.Bignum.Parameters.limb_logand",
"typing_Hacl.Bignum.Parameters.v"
],
0
],
[
"Hacl.Spec.EC.Format.fexpand_spec",
5,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fexpand_spec",
6,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fexpand_spec",
7,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fexpand_spec",
8,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fexpand_spec",
9,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.nineteen",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.nineteen",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt64.t",
"equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.uint64_to_limb",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.Fsquare.p64",
"equation_Hacl.Spec.Bignum.Modulo.nineteen", "equation_Prims.pos",
"function_token_typing_Hacl.Spec.Bignum.Fsquare.p64",
"function_token_typing_Hacl.Spec.Bignum.Modulo.nineteen",
"proj_equation_FStar.UInt64.Mk_v",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt64.Mk_v",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_da98c95d2af35788da839c6c05bdbc1c",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_7bd5fa9c50dae16a8da2d2f2cd22cf6e"
],
0
],
[
"Hacl.Spec.EC.Format.lemma_carry_local",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_carry_local",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.EC.AddAndDouble.p51", "equation_Prims.nat",
"equation_Prims.pos",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Hacl.Spec.EC.Format.lemma_carry_local",
3,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_FStar.Mul.op_Star",
"equation_Hacl.Spec.EC.AddAndDouble.p51", "equation_Prims.nat",
"equation_Prims.pos",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
1,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.Format.p51", "equation_Prims.pos",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.t",
"equation_FStar.UInt64.t", "equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.limb_size",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.logand", "equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Limb.op_Amp_Hat",
"equation_Hacl.Bignum.Limb.op_Greater_Greater_Hat",
"equation_Hacl.Bignum.Limb.op_Plus_Hat",
"equation_Hacl.Bignum.Limb.t", "equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.climb_size",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.seqelem",
"equation_Hacl.Bignum.Parameters.v",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Spec.Bignum.Fsquare.p64",
"equation_Hacl.Spec.Bignum.Modulo.mask_51",
"equation_Hacl.Spec.EC.AddAndDouble.bounds",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.AddAndDouble.p513",
"equation_Hacl.Spec.EC.AddAndDouble.red_513",
"equation_Hacl.Spec.EC.Format.mask_51",
"equation_Hacl.Spec.EC.Format.p51",
"equation_Hacl.Spec.EC.Format.seq_upd_5", "equation_Prims.pos",
"function_token_typing_Hacl.Bignum.Parameters.climb_size",
"function_token_typing_Hacl.Spec.Bignum.Fsquare.p64",
"function_token_typing_Hacl.Spec.Bignum.Modulo.mask_51",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"function_token_typing_Hacl.Spec.EC.Format.mask_51", "int_inversion",
"int_typing", "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",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_a30e8d969265dbda4e27b2da53852f2c",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_af3a13b4eecac03b78c491f7ef2b46d1",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_da98c95d2af35788da839c6c05bdbc1c",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_ebf171ea18a7d062213a1b4483bc8ed1",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_8ed80e5754ec40c80bc8e499121644eb",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_0957416e4227d4c2de7ea31c497560ef",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_2f0f8886203f3b0177e862b92a1d41c8",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_fbeb948e7b55d26b356be9c295cf3ca6",
"typing_Hacl.Bignum.Limb.v",
"typing_Hacl.Bignum.Parameters.limb_logand",
"typing_Hacl.Bignum.Parameters.v"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
4,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
5,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
6,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
7,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
8,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
9,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
10,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
11,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
12,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
13,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_pass",
14,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_full",
1,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Parameters.prime",
"equation_Hacl.Spec.Bignum.elem",
"haseqHacl.Spec.Bignum.Field_Tm_refine_64fde586cd61a9af199b0a72fdba45d1"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_full",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.AddAndDouble.p52",
"equation_Hacl.Spec.EC.Format.p51", "equation_Prims.pos",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p52",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_0687947f194c800b72626856850fce93",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_first_carry_full",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.UInt32_interpretation_Tm_arrow_15569832cb7b48ce3fe999c98911dd3f",
"FStar.UInt64_interpretation_Tm_arrow_0341c6333c4daf9671e1676b22c1a20e",
"Hacl.Bignum.Limb_interpretation_Tm_arrow_a678d40050aed93bdb88eef7c3fa3ba6",
"Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
"b2t_def", "bool_inversion", "bool_typing",
"data_elim_FStar.UInt64.Mk", "equation_FStar.Mul.op_Star",
"equation_FStar.UInt.add", "equation_FStar.UInt.fits",
"equation_FStar.UInt.logand", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.shift_right",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.t", "equation_FStar.UInt64.add",
"equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_right",
"equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t",
"equation_FStar.UInt64.v", "equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.limb_size",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.add", "equation_Hacl.Bignum.Limb.logand",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Limb.op_Amp_Hat",
"equation_Hacl.Bignum.Limb.op_Greater_Greater_Hat",
"equation_Hacl.Bignum.Limb.op_Plus_Hat",
"equation_Hacl.Bignum.Limb.shift_right",
"equation_Hacl.Bignum.Limb.t", "equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.climb_size",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_add",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.limb_one",
"equation_Hacl.Bignum.Parameters.limb_shift_right",
"equation_Hacl.Bignum.Parameters.limb_zero",
"equation_Hacl.Bignum.Parameters.seqelem",
"equation_Hacl.Bignum.Parameters.uint64_to_limb",
"equation_Hacl.Bignum.Parameters.v",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.Fsquare.p64",
"equation_Hacl.Spec.Bignum.Modulo.carry_top_pre",
"equation_Hacl.Spec.Bignum.Modulo.carry_top_spec",
"equation_Hacl.Spec.Bignum.Modulo.mask_51",
"equation_Hacl.Spec.Bignum.Modulo.nineteen",
"equation_Hacl.Spec.Bignum.Modulo.two54m152",
"equation_Hacl.Spec.Bignum.selem",
"equation_Hacl.Spec.EC.AddAndDouble.bounds",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.AddAndDouble.p513",
"equation_Hacl.Spec.EC.AddAndDouble.p52",
"equation_Hacl.Spec.EC.AddAndDouble.red_513",
"equation_Hacl.Spec.EC.Format.fcontract_first_carry_pass",
"equation_Hacl.Spec.EC.Format.mask_51",
"equation_Hacl.Spec.EC.Format.nineteen",
"equation_Hacl.Spec.EC.Format.p51",
"equation_Hacl.Spec.EC.Format.seq_upd_5", "equation_Prims.nat",
"equation_Prims.pos", "function_token_typing_FStar.UInt64.n",
"function_token_typing_FStar.UInt64.shift_right",
"function_token_typing_FStar.UInt64.v",
"function_token_typing_Hacl.Bignum.Constants.limb_size",
"function_token_typing_Hacl.Bignum.Limb.op_Amp_Hat",
"function_token_typing_Hacl.Bignum.Limb.op_Greater_Greater_Hat",
"function_token_typing_Hacl.Bignum.Parameters.climb_size",
"function_token_typing_Hacl.Bignum.Parameters.limb_one",
"function_token_typing_Hacl.Bignum.Parameters.limb_zero",
"function_token_typing_Hacl.Spec.Bignum.Fsquare.p64",
"function_token_typing_Hacl.Spec.Bignum.Modulo.mask_51",
"function_token_typing_Hacl.Spec.Bignum.Modulo.nineteen",
"function_token_typing_Hacl.Spec.Bignum.Modulo.two54m152",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p52",
"function_token_typing_Hacl.Spec.EC.Format.nineteen",
"int_inversion", "int_typing", "kinding_FStar.UInt64.t_@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_len_upd",
"lemma_FStar.UInt.shift_left_value_lemma",
"lemma_FStar.UInt.shift_right_value_lemma",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt64.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt64.Mk_v",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_FStar.UInt64_Tm_refine_2cdf10a0b17b1e313a0b7d29add2d0a1",
"refinement_interpretation_FStar.UInt64_Tm_refine_647bc1e50085d38dd97fae2d2349134f",
"refinement_interpretation_FStar.UInt_Tm_refine_22e8629663f0cb1c9de86e57e73778e3",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Limb_Tm_refine_356dfd6a0a953626acf2e7152c9dda5b",
"refinement_interpretation_Hacl.Bignum.Limb_Tm_refine_845cb29d79804b7343fe68ed179f6a21",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_633aa80a196e85b97edd2967187cb9b6",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_72320aff465f8f5be1a60f01274a9fe3",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_a30e8d969265dbda4e27b2da53852f2c",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_af3a13b4eecac03b78c491f7ef2b46d1",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_b6cddb0925a26b22bc7c5884d275beb2",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_e1b2b14c635fa5711536b20ff4a3fd24",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_eefb61e8c886ece20b4be747b20f60f5",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_da98c95d2af35788da839c6c05bdbc1c",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_22041ac5cef977a2fe214c708c282dde",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_7bd5fa9c50dae16a8da2d2f2cd22cf6e",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_ebf171ea18a7d062213a1b4483bc8ed1",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_0687947f194c800b72626856850fce93",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_8ed80e5754ec40c80bc8e499121644eb",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_24ce0951f82601fdadbdf8d924169c27",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_dfc77daf09fb145518bfdb54ca2d15fb",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_f90236f1677bfcf8f5747e513d9e3b4c",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_FStar.UInt64.shift_right",
"token_correspondence_FStar.UInt64.v",
"token_correspondence_Hacl.Bignum.Limb.op_Amp_Hat",
"token_correspondence_Hacl.Bignum.Limb.op_Greater_Greater_Hat",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.upd",
"typing_FStar.UInt.add", "typing_FStar.UInt.fits",
"typing_FStar.UInt.shift_right",
"typing_FStar.UInt64.__proj__Mk__item__v", "typing_FStar.UInt64.add",
"typing_Hacl.Bignum.Limb.op_Amp_Hat",
"typing_Hacl.Bignum.Limb.op_Greater_Greater_Hat",
"typing_Hacl.Bignum.Limb.op_Less_Less_Hat",
"typing_Hacl.Bignum.Parameters.limb_add",
"typing_Hacl.Bignum.Parameters.limb_logand",
"typing_Hacl.Bignum.Parameters.limb_shift_right",
"typing_Hacl.Bignum.Parameters.v",
"typing_Hacl.Spec.EC.Format.seq_upd_5"
],
0
],
[
"Hacl.Spec.EC.Format.lemma_div_51",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.EC.AddAndDouble.p51", "equation_Prims.nat",
"equation_Prims.pos",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"int_inversion", "primitive_Prims.op_Division",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_42dfd8c94e13dea42e85cee167c4d3be",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Hacl.Spec.EC.Format.lemma_div_51",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_div_51",
3,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"haseqHacl.Spec.EC.Format_Tm_refine_d74a7d0063d28a4eb4c82cec4e8b4091",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.lemma_div_51",
4,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_div_51",
5,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_div_51",
6,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"haseqHacl.Spec.EC.Format_Tm_refine_d74a7d0063d28a4eb4c82cec4e8b4091",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
1,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"haseqHacl.Spec.EC.Format_Tm_refine_e3e6806fa7af5cc9173ef13bc775aaf5",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
2,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt64.t",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.seqelem",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.Format.p51", "equation_Prims.pos",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
4,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"data_elim_FStar.UInt64.Mk", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.t", "equation_FStar.UInt64.logand",
"equation_FStar.UInt64.n", "equation_FStar.UInt64.t",
"equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.limb_size",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.logand", "equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Limb.op_Amp_Hat",
"equation_Hacl.Bignum.Limb.op_Greater_Greater_Hat",
"equation_Hacl.Bignum.Limb.op_Plus_Hat",
"equation_Hacl.Bignum.Limb.t", "equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.climb_size",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_logand",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.seqelem",
"equation_Hacl.Bignum.Parameters.uint64_to_limb",
"equation_Hacl.Bignum.Parameters.v",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.Fsquare.p64",
"equation_Hacl.Spec.Bignum.Modulo.mask_51",
"equation_Hacl.Spec.Bignum.Modulo.two54m152",
"equation_Hacl.Spec.EC.AddAndDouble.bounds",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.AddAndDouble.p52",
"equation_Hacl.Spec.EC.Format.mask_51",
"equation_Hacl.Spec.EC.Format.p51",
"equation_Hacl.Spec.EC.Format.seq_upd_5", "equation_Prims.pos",
"function_token_typing_Hacl.Bignum.Parameters.climb_size",
"function_token_typing_Hacl.Spec.Bignum.Fsquare.p64",
"function_token_typing_Hacl.Spec.Bignum.Modulo.mask_51",
"function_token_typing_Hacl.Spec.Bignum.Modulo.two54m152",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p52",
"function_token_typing_Hacl.Spec.EC.Format.mask_51", "int_inversion",
"int_typing", "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",
"proj_equation_FStar.UInt64.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt64.Mk_v",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_a30e8d969265dbda4e27b2da53852f2c",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_af3a13b4eecac03b78c491f7ef2b46d1",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_da98c95d2af35788da839c6c05bdbc1c",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_22041ac5cef977a2fe214c708c282dde",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_ebf171ea18a7d062213a1b4483bc8ed1",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_0687947f194c800b72626856850fce93",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_0957416e4227d4c2de7ea31c497560ef",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_2f0f8886203f3b0177e862b92a1d41c8",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_c5bb71ab92f719a0da614dc4ad40b5dd",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_fbeb948e7b55d26b356be9c295cf3ca6",
"typing_Hacl.Bignum.Limb.v",
"typing_Hacl.Bignum.Parameters.limb_logand",
"typing_Hacl.Bignum.Parameters.v"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
5,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
6,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
7,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
8,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
9,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
10,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
11,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
12,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
13,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
14,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
15,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_pass",
16,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_full",
1,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Parameters.prime",
"equation_Hacl.Spec.Bignum.elem",
"haseqHacl.Spec.Bignum.Field_Tm_refine_64fde586cd61a9af199b0a72fdba45d1"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_full",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.Format.p51", "equation_Prims.pos",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_second_carry_full",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_bdcbfedb2f96eeeeff6f38aed48c66a0",
"FStar.UInt32_interpretation_Tm_arrow_15569832cb7b48ce3fe999c98911dd3f",
"FStar.UInt64_interpretation_Tm_arrow_e22e1e7f6400a4aea7a5ff855da477b4",
"Hacl.Bignum.Limb_interpretation_Tm_arrow_1d5a7f2299b319c7faad990ba5deec17",
"Hacl.Bignum.Parameters_interpretation_Tm_arrow_68287c407519b9b219b501c88dee4f78",
"Hacl.Bignum.Parameters_interpretation_Tm_arrow_a0b527118d045c169a779a8f4f2ea57a",
"Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
"b2t_def", "bool_inversion", "bool_typing",
"data_elim_FStar.UInt64.Mk", "data_typing_intro_FStar.UInt64.Mk@tok",
"equation_FStar.Int63.n", "equation_FStar.UInt.add",
"equation_FStar.UInt.fits", "equation_FStar.UInt.logand",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.mul", "equation_FStar.UInt.shift_right",
"equation_FStar.UInt.size", "equation_FStar.UInt.sub",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_FStar.UInt32.t", "equation_FStar.UInt64.add",
"equation_FStar.UInt64.logand", "equation_FStar.UInt64.mul",
"equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_right",
"equation_FStar.UInt64.sub", "equation_FStar.UInt64.t",
"equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.limb_size",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.add", "equation_Hacl.Bignum.Limb.logand",
"equation_Hacl.Bignum.Limb.mul", "equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Limb.op_Amp_Hat",
"equation_Hacl.Bignum.Limb.op_Greater_Greater_Hat",
"equation_Hacl.Bignum.Limb.op_Less_Less_Hat",
"equation_Hacl.Bignum.Limb.op_Plus_Hat",
"equation_Hacl.Bignum.Limb.op_Star_Hat",
"equation_Hacl.Bignum.Limb.op_Subtraction_Hat",
"equation_Hacl.Bignum.Limb.shift_right",
"equation_Hacl.Bignum.Limb.sub", "equation_Hacl.Bignum.Limb.t",
"equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.climb_size",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_add",
"equation_Hacl.Bignum.Parameters.limb_logand",
"equation_Hacl.Bignum.Parameters.limb_mul",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.limb_one",
"equation_Hacl.Bignum.Parameters.limb_shift_right",
"equation_Hacl.Bignum.Parameters.limb_sub",
"equation_Hacl.Bignum.Parameters.limb_zero",
"equation_Hacl.Bignum.Parameters.seqelem",
"equation_Hacl.Bignum.Parameters.uint64_to_limb",
"equation_Hacl.Bignum.Parameters.v",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.Fproduct.carry_0_to_1_pre",
"equation_Hacl.Spec.Bignum.Fproduct.carry_0_to_1_spec",
"equation_Hacl.Spec.Bignum.Fsquare.p64",
"equation_Hacl.Spec.Bignum.Modulo.carry_top_pre",
"equation_Hacl.Spec.Bignum.Modulo.carry_top_spec",
"equation_Hacl.Spec.Bignum.Modulo.mask_51",
"equation_Hacl.Spec.Bignum.Modulo.nineteen",
"equation_Hacl.Spec.Bignum.Modulo.two54m152",
"equation_Hacl.Spec.Bignum.selem",
"equation_Hacl.Spec.EC.AddAndDouble.bounds",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.AddAndDouble.p52",
"equation_Hacl.Spec.EC.Format.fcontract_second_carry_pass",
"equation_Hacl.Spec.EC.Format.mask_51",
"equation_Hacl.Spec.EC.Format.nineteen",
"equation_Hacl.Spec.EC.Format.p51",
"equation_Hacl.Spec.EC.Format.seq_upd_5", "equation_Prims.nat",
"equation_Prims.pos", "fuel_guarded_inversion_FStar.UInt64.t_",
"function_token_typing_FStar.Int63.n",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_FStar.UInt64.n",
"function_token_typing_FStar.UInt64.shift_right",
"function_token_typing_Hacl.Bignum.Constants.limb_size",
"function_token_typing_Hacl.Bignum.Limb.op_Amp_Hat",
"function_token_typing_Hacl.Bignum.Limb.op_Greater_Greater_Hat",
"function_token_typing_Hacl.Bignum.Limb.v",
"function_token_typing_Hacl.Bignum.Parameters.climb_size",
"function_token_typing_Hacl.Bignum.Parameters.limb_logand",
"function_token_typing_Hacl.Bignum.Parameters.limb_one",
"function_token_typing_Hacl.Bignum.Parameters.limb_shift_right",
"function_token_typing_Hacl.Bignum.Parameters.limb_zero",
"function_token_typing_Hacl.Spec.Bignum.Fsquare.p64",
"function_token_typing_Hacl.Spec.Bignum.Modulo.mask_51",
"function_token_typing_Hacl.Spec.Bignum.Modulo.nineteen",
"function_token_typing_Hacl.Spec.Bignum.Modulo.two54m152",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p52",
"function_token_typing_Hacl.Spec.EC.Format.mask_51",
"function_token_typing_Hacl.Spec.EC.Format.nineteen",
"int_inversion", "int_typing", "kinding_FStar.UInt64.t_@tok",
"lemma_FStar.Buffer.lemma_size",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_upd", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt.shift_right_value_lemma",
"lemma_Hacl.Bignum.Parameters.lemma_limb_injectivity",
"lemma_Hacl.Spec.Bignum.Fsum.lemma_mod",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt64.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt64.Mk_v",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
"refinement_interpretation_FStar.UInt64_Tm_refine_5c114bc17b55577083d2f1232d5b463f",
"refinement_interpretation_FStar.UInt64_Tm_refine_647bc1e50085d38dd97fae2d2349134f",
"refinement_interpretation_FStar.UInt64_Tm_refine_9bd11efd3d1b15018e7a1047644f241f",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Limb_Tm_refine_13e2b4532d01e8922cfa27b90315122c",
"refinement_interpretation_Hacl.Bignum.Limb_Tm_refine_60b351bc6357b4b54fa5c4d0e4fadc09",
"refinement_interpretation_Hacl.Bignum.Limb_Tm_refine_b625cb3f3898b45f2fe6af01f64ae5d5",
"refinement_interpretation_Hacl.Bignum.Limb_Tm_refine_b7e051cee3a61863c1b7e4c0d9be7008",
"refinement_interpretation_Hacl.Bignum.Limb_Tm_refine_cc8f63b87ec0708e797ae8c1f89eb866",
"refinement_interpretation_Hacl.Bignum.Limb_Tm_refine_ff32416a5859ec7d24bb659678c05708",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_67fc71e1b4022b6371625644ad1ad89f",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_72320aff465f8f5be1a60f01274a9fe3",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_a30e8d969265dbda4e27b2da53852f2c",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_af3a13b4eecac03b78c491f7ef2b46d1",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_b6cddb0925a26b22bc7c5884d275beb2",
"refinement_interpretation_Hacl.Spec.Bignum.Fproduct_Tm_refine_309bd01ae86f04be15be0d04630f43d6",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_da98c95d2af35788da839c6c05bdbc1c",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_22041ac5cef977a2fe214c708c282dde",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_7bd5fa9c50dae16a8da2d2f2cd22cf6e",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_ebf171ea18a7d062213a1b4483bc8ed1",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_0687947f194c800b72626856850fce93",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_0957416e4227d4c2de7ea31c497560ef",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_24ce0951f82601fdadbdf8d924169c27",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_4be396be9b38925683e155dbbcdd04b9",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_c5bb71ab92f719a0da614dc4ad40b5dd",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_f90236f1677bfcf8f5747e513d9e3b4c",
"refinement_interpretation_Hacl.UInt128_Tm_refine_5b2ad87cd68494149f9a9229c91e04a2",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_FStar.Seq.Base.index",
"token_correspondence_FStar.UInt64.shift_right",
"token_correspondence_Hacl.Bignum.Limb.op_Amp_Hat",
"token_correspondence_Hacl.Bignum.Limb.op_Greater_Greater_Hat",
"token_correspondence_Hacl.Bignum.Limb.v",
"token_correspondence_Hacl.Bignum.Parameters.limb_logand",
"token_correspondence_Hacl.Bignum.Parameters.limb_shift_right",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.upd",
"typing_FStar.UInt.fits", "typing_FStar.UInt.logand",
"typing_FStar.UInt.shift_right", "typing_FStar.UInt32.v",
"typing_FStar.UInt64.__proj__Mk__item__v", "typing_FStar.UInt64.add",
"typing_FStar.UInt64.sub", "typing_FStar.UInt64.v",
"typing_Hacl.Bignum.Limb.op_Amp_Hat",
"typing_Hacl.Bignum.Limb.op_Greater_Greater_Hat",
"typing_Hacl.Bignum.Limb.op_Less_Less_Hat",
"typing_Hacl.Bignum.Limb.op_Plus_Hat",
"typing_Hacl.Bignum.Limb.op_Subtraction_Hat",
"typing_Hacl.Bignum.Limb.v",
"typing_Hacl.Bignum.Parameters.limb_logand",
"typing_Hacl.Bignum.Parameters.limb_shift_right",
"typing_Hacl.Bignum.Parameters.v",
"typing_Hacl.Spec.EC.Format.seq_upd_5"
],
0
],
[
"Hacl.Spec.EC.Format.p51m19",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.p51m19",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.p51m19",
3,
0,
1,
[
"@query", "equation_FStar.UInt64.uint_to_t",
"equation_FStar.UInt64.v", "equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.v",
"equation_Hacl.Cast.uint64_to_sint64",
"proj_equation_FStar.UInt64.Mk_v",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt64.Mk_v"
],
0
],
[
"Hacl.Spec.EC.Format.p51m1",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.p51m1",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.p51m1",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt64.t",
"equation_Hacl.Bignum.Constants.limb", "equation_Hacl.Bignum.Limb.t",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.uint64_to_limb",
"equation_Hacl.Spec.EC.Format.mask_51",
"function_token_typing_Hacl.Spec.EC.Format.mask_51",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_0957416e4227d4c2de7ea31c497560ef"
],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_1",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_1",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_1",
3,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_1",
4,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_1",
5,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Parameters.prime",
"haseqHacl.Spec.EC.Format_Tm_refine_7e377836eff1cae79828ae1aaffc5666"
],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_1",
6,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt64.t",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.seqelem",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.Format.p51", "equation_Prims.pos",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2"
],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_1",
7,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_FStar.Mul.op_Star", "equation_FStar.UInt64.t",
"equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.prime",
"equation_Hacl.Bignum.Parameters.uint64_to_limb",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.Field.elem",
"equation_Hacl.Spec.Bignum.Field.one",
"equation_Hacl.Spec.Bignum.Modulo.mask_51",
"equation_Hacl.Spec.Bignum.selem",
"equation_Hacl.Spec.EC.AddAndDouble.bounds",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.Format.p51",
"equation_Hacl.Spec.EC.Format.p51m1", "equation_Prims.pos",
"function_token_typing_Hacl.Spec.Bignum.Field.one",
"function_token_typing_Hacl.Spec.Bignum.Modulo.mask_51",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"function_token_typing_Hacl.Spec.EC.Format.p51m1",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt64.Mk_v",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt64.Mk_v",
"refinement_interpretation_Hacl.Spec.Bignum.Field_Tm_refine_64fde586cd61a9af199b0a72fdba45d1",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_ebf171ea18a7d062213a1b4483bc8ed1",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_0957416e4227d4c2de7ea31c497560ef"
],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_1",
8,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_1",
9,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_1",
10,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_1",
11,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_1",
12,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
3,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
4,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
5,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
6,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Parameters.prime",
"equation_Hacl.Spec.Bignum.Field.elem",
"equation_Hacl.Spec.Bignum.Field.one",
"function_token_typing_Hacl.Spec.Bignum.Field.one",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Hacl.Spec.Bignum.Field_Tm_refine_64fde586cd61a9af199b0a72fdba45d1"
],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
7,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "data_elim_FStar.UInt64.Mk",
"equation_FStar.HyperHeap.test0", "equation_FStar.Mul.op_Star",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt64.n",
"equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t",
"equation_FStar.UInt64.v", "equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n", "equation_Hacl.Bignum.Limb.t",
"equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.prime",
"equation_Hacl.Bignum.Parameters.uint64_to_limb",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.Fsquare.p64",
"equation_Hacl.Spec.Bignum.Modulo.two54m152",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.Format.p51m1", "equation_Prims._assert",
"equation_Prims.pos", "fuel_guarded_inversion_FStar.UInt64.t_",
"function_token_typing_FStar.HyperHeap.test0",
"function_token_typing_Hacl.Spec.Bignum.Fsquare.p64",
"function_token_typing_Hacl.Spec.Bignum.Modulo.two54m152",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"function_token_typing_Hacl.Spec.EC.Format.p51m1",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_FStar.UInt64.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt64.Mk_v",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_da98c95d2af35788da839c6c05bdbc1c",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_22041ac5cef977a2fe214c708c282dde",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_0957416e4227d4c2de7ea31c497560ef",
"typing_Hacl.Bignum.Limb.v"
],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
8,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
9,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
10,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
11,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
12,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
13,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
14,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
15,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
16,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.lemma_fcontract_trim_2",
17,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
1,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Parameters.prime",
"haseqHacl.Spec.EC.Format_Tm_refine_7e377836eff1cae79828ae1aaffc5666"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.Format.p51", "equation_Prims.pos",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "data_elim_FStar.UInt64.Mk", "equation_FStar.UInt.fits",
"equation_FStar.UInt.logand", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.ones",
"equation_FStar.UInt.size", "equation_FStar.UInt.sub",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt.zero",
"equation_FStar.UInt64.logand", "equation_FStar.UInt64.n",
"equation_FStar.UInt64.sub", "equation_FStar.UInt64.t",
"equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.eq_mask",
"equation_Hacl.Bignum.Limb.logand", "equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Limb.op_Amp_Hat",
"equation_Hacl.Bignum.Limb.op_Subtraction_Hat",
"equation_Hacl.Bignum.Limb.sub", "equation_Hacl.Bignum.Limb.t",
"equation_Hacl.Bignum.Limb.v", "equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_logand",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.limb_sub",
"equation_Hacl.Bignum.Parameters.limb_zero",
"equation_Hacl.Bignum.Parameters.prime",
"equation_Hacl.Bignum.Parameters.seqelem",
"equation_Hacl.Bignum.Parameters.uint64_to_limb",
"equation_Hacl.Bignum.Parameters.v",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.Fsquare.p64",
"equation_Hacl.Spec.Bignum.Modulo.mask_51",
"equation_Hacl.Spec.Bignum.Modulo.two54m152",
"equation_Hacl.Spec.Bignum.elem", "equation_Hacl.Spec.Bignum.selem",
"equation_Hacl.Spec.EC.AddAndDouble.bounds",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.Format.p51",
"equation_Hacl.Spec.EC.Format.p51m1",
"equation_Hacl.Spec.EC.Format.p51m19",
"equation_Hacl.Spec.EC.Format.seq_upd_5", "equation_Prims.nat",
"equation_Prims.pos", "fuel_guarded_inversion_FStar.UInt64.t_",
"function_token_typing_Hacl.Bignum.Parameters.limb_zero",
"function_token_typing_Hacl.Spec.Bignum.Fsquare.p64",
"function_token_typing_Hacl.Spec.Bignum.Modulo.mask_51",
"function_token_typing_Hacl.Spec.Bignum.Modulo.two54m152",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"function_token_typing_Hacl.Spec.EC.Format.p51m1",
"function_token_typing_Hacl.Spec.EC.Format.p51m19", "int_inversion",
"int_typing", "lemma_Hacl.Bignum.Parameters.lemma_limb_injectivity",
"lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
"proj_equation_FStar.UInt64.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt64.Mk_v",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Limb_Tm_refine_454eeb27d72c225d30b80494074a314b",
"refinement_interpretation_Hacl.Bignum.Limb_Tm_refine_60b351bc6357b4b54fa5c4d0e4fadc09",
"refinement_interpretation_Hacl.Bignum.Limb_Tm_refine_8f20aa2d110a537c26a2ee9aa210d6f3",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_317595f12a45eeb1284b89bf0ca985c9",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_72320aff465f8f5be1a60f01274a9fe3",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_af3a13b4eecac03b78c491f7ef2b46d1",
"refinement_interpretation_Hacl.Spec.Bignum.Field_Tm_refine_64fde586cd61a9af199b0a72fdba45d1",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_da98c95d2af35788da839c6c05bdbc1c",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_22041ac5cef977a2fe214c708c282dde",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_ebf171ea18a7d062213a1b4483bc8ed1",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_0957416e4227d4c2de7ea31c497560ef",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_2367330f0862e94e660acad91e32c272",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_24ce0951f82601fdadbdf8d924169c27",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_36482805a3ed12e482ccc8a2164cc0a7",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_8d889fd52fee11923c6fecb5f9f9a618",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_9953eeabfb9e130245e11967be0915ee",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_e3c618a8c7023f0b27c5f31b54e7292a",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_fcc0534ca6076f7d811b2032a9c575e1",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.UInt64.v", "typing_Hacl.Bignum.Limb.eq_mask",
"typing_Hacl.Bignum.Limb.gte_mask",
"typing_Hacl.Bignum.Limb.op_Amp_Hat", "typing_Hacl.Bignum.Limb.v",
"typing_Hacl.Bignum.Parameters.limb_eq_mask",
"typing_Hacl.Bignum.Parameters.limb_logand",
"typing_Hacl.Bignum.Parameters.v", "typing_Hacl.Spec.Bignum.selem",
"typing_Hacl.Spec.EC.Format.seq_upd_5"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
4,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
5,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
6,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
7,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
8,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
9,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
10,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
11,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
12,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
13,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
14,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"haseqHacl.Spec.EC.Format_Tm_refine_b34ab48900043a6c20e7f1569c75ad15",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
15,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"haseqHacl.Spec.EC.Format_Tm_refine_b34ab48900043a6c20e7f1569c75ad15",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
16,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"haseqHacl.Spec.EC.Format_Tm_refine_b34ab48900043a6c20e7f1569c75ad15",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
17,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
18,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
19,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
20,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
21,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"haseqHacl.Spec.EC.Format_Tm_refine_b34ab48900043a6c20e7f1569c75ad15",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
22,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
23,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
24,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
25,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
26,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
27,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
28,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
29,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
30,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
31,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
32,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
33,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
34,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"haseqFStar.UInt_Tm_refine_81528fa45830671a34dc41538a864b77",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
35,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"haseqFStar.UInt_Tm_refine_81528fa45830671a34dc41538a864b77",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
36,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"haseqFStar.UInt_Tm_refine_81528fa45830671a34dc41538a864b77",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
37,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"haseqFStar.UInt_Tm_refine_81528fa45830671a34dc41538a864b77",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
38,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"haseqFStar.UInt_Tm_refine_81528fa45830671a34dc41538a864b77",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
39,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
40,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
41,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_trim",
42,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store_lemma",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store_lemma",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_FStar.UInt32.t", "equation_FStar.UInt32.v",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"lemma_FStar.Buffer.lemma_size",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_251f849c8185346dc81059d89f7d014c",
"typing_FStar.UInt32.v"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store_lemma",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "data_elim_FStar.UInt32.Mk", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_FStar.UInt32.t", "equation_FStar.UInt32.v",
"equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_right",
"equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Limb.op_Greater_Greater_Hat",
"equation_Hacl.Bignum.Limb.shift_right",
"equation_Hacl.Bignum.Limb.t", "equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.limb_shift_right",
"equation_Hacl.Bignum.Parameters.v",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Spec.Bignum.Fsquare.p64", "equation_Prims.nat",
"equation_Prims.pos", "fuel_guarded_inversion_FStar.UInt32.t_",
"fuel_guarded_inversion_FStar.UInt64.t_",
"function_token_typing_FStar.UInt64.n",
"function_token_typing_Hacl.Spec.Bignum.Fsquare.p64",
"lemma_FStar.Buffer.lemma_size",
"lemma_FStar.UInt.shift_right_value_lemma",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
"proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt64.Mk_v",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Limb_Tm_refine_b7e051cee3a61863c1b7e4c0d9be7008",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_da98c95d2af35788da839c6c05bdbc1c",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_251f849c8185346dc81059d89f7d014c",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_921535e5834c0f612ba5e2e161c346e2",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_ee8dd5a78c34dda9bc154a9fab8b6681",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.UInt32.v"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store_lemma",
4,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store_lemma",
5,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store",
2,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.Format.p51", "equation_Prims.pos",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store",
4,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"data_elim_FStar.UInt64.Mk", "equation_FStar.Seq.Base.op_At_Bar",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
"equation_FStar.UInt32.v", "equation_FStar.UInt64.logor",
"equation_FStar.UInt64.n", "equation_FStar.UInt64.t",
"equation_FStar.UInt8.t", "equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.limb_size",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.logor", "equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Limb.op_Bar_Hat",
"equation_Hacl.Bignum.Limb.t", "equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Parameters.climb_size",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_logor",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.seqelem",
"equation_Hacl.Bignum.Parameters.v",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Spec.EC.AddAndDouble.bounds",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.Format.p51",
"equation_Hacl.Spec.EC.Format.store64_le_spec",
"equation_Hacl.Spec.EC.Format.uint8_s", "equation_Prims.nat",
"equation_Prims.pos", "fuel_guarded_inversion_FStar.UInt64.t_",
"function_token_typing_Hacl.Bignum.Parameters.climb_size",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"int_inversion", "int_typing", "kinding_FStar.UInt8.t_@tok",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt32.Mk_v",
"projection_inverse_FStar.UInt64.Mk_v",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_a14797a977f3a3617ca23dd3dce65211",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_a30e8d969265dbda4e27b2da53852f2c",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_1e595318842fac1d9b987169bb7bb84b",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_36482805a3ed12e482ccc8a2164cc0a7",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_5ef4cda51905fa6c0b26314bed084dce",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_6aecaa006efc11f9011ec564fac60a98",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_7d0dfbd57128ac2f6801d6f3eb677898",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_b00ecc56c9382d1623f995ad21746e44",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_bdc254ef4d4e510e45d84fd4e96ba4b5",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_e20faa8fefe44111594bdcf95138a00f",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_f5185a507965212de13621329197755a",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Bignum.Parameters.limb_logor",
"typing_Hacl.Bignum.Parameters.v"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store",
5,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store",
6,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store",
7,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store",
8,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_store",
9,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.word_size",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_spec",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.fcontract_spec",
2,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Parameters.prime",
"haseqHacl.Spec.EC.Format_Tm_refine_7e377836eff1cae79828ae1aaffc5666"
],
0
],
[
"Hacl.Spec.EC.Format.fcontract_spec",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Bignum.Parameters.seqelem",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.Format.p51",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_0189fac664ff0b0a8f370377880240db",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_29facbbb0976fdd879c73b3a3008b4e3",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_cd8bb6f69b28ac1b8f76e380fb0b3f95"
],
0
],
[
"Hacl.Spec.EC.Format.point_of_scalar",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.point_of_scalar",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.point_of_scalar",
3,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.point_of_scalar",
4,
0,
1,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0
],
[
"Hacl.Spec.EC.Format.point_of_scalar",
5,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.Mul.op_Star",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.v",
"equation_FStar.UInt64.n", "equation_FStar.UInt64.t",
"equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt8.n",
"equation_FStar.UInt8.t", "equation_Hacl.Bignum.Constants.keylen",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.n", "equation_Hacl.Bignum.Limb.t",
"equation_Hacl.Bignum.Limb.v", "equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.limb_one",
"equation_Hacl.Bignum.Parameters.limb_zero",
"equation_Hacl.Bignum.Parameters.prime",
"equation_Hacl.Bignum.Parameters.seqelem",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.selem",
"equation_Hacl.Spec.EC.AddAndDouble.bounds",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.AddAndDouble.p513",
"equation_Hacl.Spec.EC.AddAndDouble.red_513",
"equation_Hacl.Spec.EC.Format.fexpand_spec",
"equation_Hacl.Spec.EC.Format.uint8_s", "equation_Prims.nat",
"equation_Prims.pos", "function_token_typing_FStar.UInt8.n",
"function_token_typing_Hacl.Bignum.Parameters.limb_one",
"function_token_typing_Hacl.Bignum.Parameters.limb_zero",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"int_inversion", "int_typing", "kinding_FStar.UInt64.t_@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Base.lemma_len_upd", "lemma_FStar.UInt.pow2_values",
"lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_FStar.UInt32.Mk_v",
"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.UInt32.Mk_v",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_72320aff465f8f5be1a60f01274a9fe3",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_b6cddb0925a26b22bc7c5884d275beb2",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_7af23035b9e3fabcc3b2b6d79157bb7e",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_Hacl.Bignum.Limb.v"
],
0
],
[
"Hacl.Spec.EC.Format.scalar_of_point",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.scalar_of_point",
2,
0,
1,
[
"@query", "equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Parameters.prime",
"equation_Spec.Curve25519.prime"
],
0
],
[
"Hacl.Spec.EC.Format.scalar_of_point",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_correspondence_Spec.Curve25519.op_Star_Star.fuel_instrumented",
"@query", "b2t_def", "equation_FStar.Mul.op_Star",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
"equation_FStar.UInt8.n", "equation_FStar.UInt8.t",
"equation_Hacl.Bignum.Constants.keylen",
"equation_Hacl.Bignum.Constants.limb_size",
"equation_Hacl.Bignum.Constants.prime",
"equation_Hacl.Bignum.Parameters.climb_size",
"equation_Hacl.Bignum.Parameters.prime",
"equation_Hacl.Bignum.Parameters.seqelem",
"equation_Hacl.Spec.Bignum.Crecip.crecip_tot",
"equation_Hacl.Spec.Bignum.Crecip.s_513",
"equation_Hacl.Spec.Bignum.Fmul.fmul_spec",
"equation_Hacl.Spec.Bignum.fmul",
"equation_Hacl.Spec.Bignum.fmul_tot",
"equation_Hacl.Spec.Bignum.op_Star_At",
"equation_Hacl.Spec.EC.Format.uint8_s",
"equation_Hacl.Spec.EC.Point.sgetx",
"equation_Hacl.Spec.EC.Point.sgetz",
"equation_Hacl.Spec.EC.Point.spoint",
"equation_Hacl.Spec.EC.Point.spoint_513", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.Curve25519.encodePoint",
"equation_Spec.Curve25519.fmul",
"equation_Spec.Curve25519.op_Star_At",
"equation_Spec.Curve25519.prime",
"equation_Spec.Curve25519.serialized_point",
"equation_Spec.Lib.lbytes",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_Hacl.Bignum.Parameters.climb_size",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
"lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.Curve25519.Proj_x",
"proj_equation_Spec.Curve25519.Proj_z",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.Curve25519.Proj_x",
"projection_inverse_Spec.Curve25519.Proj_z",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_a30e8d969265dbda4e27b2da53852f2c",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_8ed80e5754ec40c80bc8e499121644eb",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_1510ece45e940b32041fd4e58148dab3",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_97e694050036fe92a944353502dfceaf",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_bc0997f22510438a59a07b1f5bbdddcc",
"refinement_interpretation_Hacl.Spec.EC.Format_Tm_refine_dd2c956b359a453dc9f1d438287ecba4",
"refinement_interpretation_Hacl.Spec.EC.Point_Tm_refine_e1321e32f4ab7518c096a1967fe8a338",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
"typing_Prims.pow2"
],
0
],
[
"Hacl.Spec.EC.Format.scalar_of_point",
4,
0,
1,
[
"@query", "assumption_Prims.HasEq_int",
"equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v",
"equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt32.Mk_v"
],
0
],
[
"Hacl.Spec.EC.Format.scalar_of_point",
5,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.format_secret",
1,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.format_secret",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Spec.EC.Format.format_secret",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt8.t",
"equation_Hacl.Bignum.Constants.keylen",
"equation_Hacl.Spec.EC.Format.uint8_s",
"refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b"
],
0
],
[
"Hacl.Spec.EC.Format.format_secret",
4,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "data_elim_FStar.UInt64.Mk",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt64.n",
"equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t",
"equation_FStar.UInt64.v", "equation_FStar.UInt8.logand",
"equation_FStar.UInt8.logor", "equation_FStar.UInt8.n",
"equation_FStar.UInt8.t", "equation_FStar.UInt8.uint_to_t",
"equation_FStar.UInt8.v", "equation_Hacl.Bignum.Constants.keylen",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.uint64_to_limb",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Cast.uint8_to_sint8",
"equation_Hacl.Spec.Bignum.Modulo.two54m152",
"equation_Hacl.Spec.EC.Format.uint8_s", "equation_Prims.nat",
"equation_Spec.Curve25519.decodeScalar25519",
"equation_Spec.Lib.op_String_Access",
"equation_Spec.Lib.op_String_Assignment",
"function_token_typing_FStar.UInt64.n",
"function_token_typing_Hacl.Spec.Bignum.Modulo.two54m152",
"int_typing", "kinding_FStar.UInt8.t_@tok",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt64.Mk_v",
"proj_equation_FStar.UInt8.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt64.Mk_v",
"projection_inverse_FStar.UInt8.Mk_v",
"refinement_interpretation_FStar.Endianness_Tm_refine_b769c0bf16cb286238e7b11ff583e99b",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
"refinement_interpretation_FStar.UInt8_Tm_refine_22871ed0ff70fd094ad3e8d742624d47",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_22041ac5cef977a2fe214c708c282dde",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.UInt8.logand", "typing_FStar.UInt8.logor",
"typing_FStar.UInt8.uint_to_t"
],
0
],
[
"Hacl.Spec.EC.Format.format_secret",
5,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
]
]
]