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.Bignum.Fsquare.fst.hints
[
"\u0012�\u000f\u0013\u0001�.�_��1l\u0007�",
[
[
"Hacl.Bignum.Fsquare.upd_5",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "assumption_Prims.HasEq_int",
"equation_FStar.UInt128.t", "equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.wide",
"equation_Hacl.Bignum.Parameters.felem_wide",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.wide", "equation_Hacl.UInt128.t",
"equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882"
],
0
],
[
"Hacl.Bignum.Fsquare.upd_5",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"data_elim_FStar.Monotonic.HyperStack.MkRef",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.contains", "equation_FStar.Buffer.idx",
"equation_FStar.Buffer.length", "equation_FStar.Buffer.live",
"equation_FStar.Buffer.sel", "equation_FStar.HyperStack.reference",
"equation_FStar.Monotonic.HyperHeap.contains_ref",
"equation_FStar.Monotonic.HyperStack.contains",
"equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n",
"equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
"equation_FStar.UInt32.v", "equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.wide",
"equation_Hacl.Bignum.Parameters.felem_wide",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.wide",
"equation_Hacl.Spec.Bignum.Fsquare.seq_upd_5",
"equation_Hacl.UInt128.t", "equation_Prims.nat",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
"fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference",
"function_token_typing_Hacl.UInt128.t", "int_inversion",
"int_typing", "lemma_FStar.Buffer.lemma_modifies_1_trans",
"lemma_FStar.Buffer.lemma_size",
"lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_FStar.Buffer.MkBuffer_content",
"proj_equation_FStar.Buffer.MkBuffer_length",
"proj_equation_FStar.Monotonic.HyperStack.MkRef_id",
"proj_equation_FStar.Monotonic.HyperStack.MkRef_ref",
"proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt32.Mk_v",
"refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"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.Fsquare_Tm_refine_75fe8a65f5666eaf920693fe19efc919",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_f927b3dfce350e2cdef0c06ac9132023",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_kinding_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d",
"typing_FStar.Buffer.__proj__MkBuffer__item__content",
"typing_FStar.Buffer.__proj__MkBuffer__item__idx",
"typing_FStar.Buffer.__proj__MkBuffer__item__length",
"typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.idx",
"typing_FStar.Monotonic.HyperStack.sel",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.upd",
"typing_FStar.UInt32.v", "typing_Hacl.Spec.Bignum.Fsquare.seq_upd_5"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare__",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "assumption_Prims.HasEq_int",
"equation_FStar.UInt128.t", "equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.wide",
"equation_Hacl.Bignum.Parameters.felem_wide",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.wide", "equation_Hacl.UInt128.t",
"equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare__",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.buffer",
"equation_FStar.UInt128.t", "equation_FStar.UInt64.t",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.wide",
"equation_Hacl.Bignum.Parameters.felem",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.wide", "equation_Hacl.UInt128.t",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_a75449b7b5f24c622e068f573fc2b030",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare__",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "data_elim_FStar.UInt64.Mk",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.mul",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v",
"equation_FStar.UInt64.mul", "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.wide",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Limb.mul", "equation_Hacl.Bignum.Limb.n",
"equation_Hacl.Bignum.Limb.op_Star_Hat",
"equation_Hacl.Bignum.Limb.t", "equation_Hacl.Bignum.Limb.v",
"equation_Hacl.Bignum.Modulo.nineteen",
"equation_Hacl.Bignum.Modulo.two54m152",
"equation_Hacl.Bignum.Parameters.felem",
"equation_Hacl.Bignum.Parameters.felem_wide",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.limb_mul",
"equation_Hacl.Bignum.Parameters.limb_n",
"equation_Hacl.Bignum.Parameters.uint64_to_limb",
"equation_Hacl.Bignum.Parameters.v",
"equation_Hacl.Bignum.Parameters.wide",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.Fsquare.fsquare_pre_",
"equation_Hacl.Spec.Bignum.Fsquare.fsquare_spec_",
"equation_Hacl.Spec.Bignum.Fsquare.p128",
"equation_Hacl.Spec.Bignum.Fsquare.p64",
"equation_Hacl.Spec.Bignum.Modulo.nineteen",
"equation_Hacl.Spec.Bignum.Modulo.two54m152",
"equation_Hacl.UInt128.t", "equation_Prims.nat",
"equation_Prims.pos", "fuel_guarded_inversion_FStar.Buffer._buffer",
"function_token_typing_Hacl.Bignum.Modulo.nineteen",
"function_token_typing_Hacl.Bignum.Modulo.two54m152",
"function_token_typing_Hacl.Spec.Bignum.Fsquare.p128",
"function_token_typing_Hacl.Spec.Bignum.Fsquare.p64",
"function_token_typing_Hacl.Spec.Bignum.Modulo.nineteen",
"function_token_typing_Hacl.Spec.Bignum.Modulo.two54m152",
"int_inversion", "int_typing", "kinding_FStar.UInt64.t_@tok",
"l_and-interp", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"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",
"projection_inverse_FStar.UInt64.Mk_v",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_1f308ce2fc46e1b89a97101f00e84b72",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_3adcb4eefad1b2624b85ad6106586f37",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_a75449b7b5f24c622e068f573fc2b030",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_fd63a68fa56fcf0785e157b67e108e4f",
"refinement_interpretation_Hacl.Bignum.Modulo_Tm_refine_2ac20c1e7708c3a206015127ba717f44",
"refinement_interpretation_Hacl.Bignum.Modulo_Tm_refine_f90236f1677bfcf8f5747e513d9e3b4c",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_33eb13346604cde889578e1fb1a22b97",
"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_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Buffer.as_seq", "typing_FStar.Seq.Base.index",
"typing_Hacl.Bignum.Limb.v"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "assumption_Prims.HasEq_int",
"equation_FStar.UInt128.t", "equation_FStar.UInt64.t",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.wide",
"equation_Hacl.Bignum.Parameters.felem",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.wide", "equation_Hacl.UInt128.t",
"equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_a75449b7b5f24c622e068f573fc2b030",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.buffer",
"equation_FStar.UInt128.t", "equation_FStar.UInt64.t",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.wide",
"equation_Hacl.Bignum.Parameters.felem",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.wide", "equation_Hacl.UInt128.t",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_a75449b7b5f24c622e068f573fc2b030",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.as_seq",
"equation_FStar.Buffer.buffer", "equation_FStar.UInt64.t",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.wide",
"equation_Hacl.Bignum.Parameters.felem",
"equation_Hacl.Bignum.Parameters.felem_wide",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.wide",
"equation_Hacl.Spec.Bignum.Fsquare.fsquare_pre",
"equation_Hacl.Spec.Bignum.Fsquare.fsquare_spec",
"equation_Hacl.UInt128.t",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
"function_token_typing_Hacl.UInt128.t",
"kinding_FStar.UInt64.t_@tok", "l_and-interp",
"lemma_FStar.Buffer.lemma_disjoint_symm",
"lemma_FStar.Buffer.lemma_modifies_1_1",
"lemma_FStar.Buffer.lemma_modifies_1_trans",
"lemma_FStar.Buffer.lemma_modifies_2_1",
"lemma_FStar.Buffer.no_upd_lemma_1",
"lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_a75449b7b5f24c622e068f573fc2b030",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882"
],
0
],
[
"Hacl.Bignum.Fsquare.relax",
1,
1,
0,
[
"@query", "equation_Hacl.Spec.EC.AddAndDouble.bounds",
"equation_Hacl.Spec.EC.AddAndDouble.p513",
"equation_Hacl.Spec.EC.AddAndDouble.p5413",
"equation_Hacl.Spec.EC.AddAndDouble.red_513",
"equation_Hacl.Spec.EC.AddAndDouble.red_5413",
"projection_inverse_BoxInt_proj_0", "unit_typing"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times_one",
1,
1,
0,
[
"@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.Bignum.Fsquare.fsquare_times_one",
2,
1,
0,
[ "@query", "projection_inverse_BoxBool_proj_0" ],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times_one",
3,
1,
0,
[
"@MaxFuel_assumption",
"@fuel_correspondence_Hacl.Spec.Bignum.Fsquare.fsquare_times_tot.fuel_instrumented",
"@query",
"equation_with_fuel_Hacl.Spec.Bignum.Fsquare.fsquare_times_tot.fuel_instrumented",
"primitive_Prims.op_Equality"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times_many",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_908043d23d9b610a14feef808af9da3d"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times_many",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.Bignum.Fsquare.fsquare_times_tot.fuel_instrumented",
"@fuel_irrelevance_Hacl.Spec.Bignum.Fsquare.fsquare_times_tot.fuel_instrumented",
"@query",
"Hacl.Bignum.Parameters_interpretation_Tm_arrow_08db2f26dd02361442f26e3240ea9976",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"b2t_def", "equation_FStar.UInt64.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.wide",
"equation_Hacl.Bignum.Constants.word_size",
"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.seqelem",
"equation_Hacl.Bignum.Parameters.seqelem_wide",
"equation_Hacl.Bignum.Parameters.v",
"equation_Hacl.Bignum.Parameters.wide",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Spec.Bignum.Fproduct.carry_wide_spec",
"equation_Hacl.Spec.Bignum.Fproduct.copy_from_wide_spec",
"equation_Hacl.Spec.Bignum.Fproduct.copy_from_wide_spec_",
"equation_Hacl.Spec.Bignum.Fsquare.fsquare_pre",
"equation_Hacl.Spec.Bignum.Fsquare.fsquare_spec",
"equation_Hacl.Spec.Bignum.Fsquare.fsquare_spec_",
"equation_Hacl.Spec.Bignum.Modulo.carry_top_wide_pre",
"equation_Hacl.Spec.Bignum.Modulo.carry_top_wide_spec",
"equation_Hacl.Spec.EC.AddAndDouble.bounds",
"equation_Hacl.Spec.EC.AddAndDouble.p51",
"equation_Hacl.Spec.EC.AddAndDouble.p513",
"equation_Hacl.Spec.EC.AddAndDouble.p5413",
"equation_Hacl.Spec.EC.AddAndDouble.red_513",
"equation_Hacl.Spec.EC.AddAndDouble.red_5413",
"equation_Hacl.UInt128.t", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Hacl.Spec.Bignum.Fsquare.fsquare_times_tot.fuel_instrumented",
"function_token_typing_Hacl.Bignum.Parameters.wide_to_limb",
"function_token_typing_Hacl.Spec.EC.AddAndDouble.p51",
"function_token_typing_Hacl.UInt128.t", "int_inversion",
"kinding_FStar.UInt64.t_@tok", "l_and-interp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Modulus", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_908043d23d9b610a14feef808af9da3d",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_d58fc10abe97ecb2e7d8d4fbd8b64788",
"refinement_interpretation_Hacl.Spec.Bignum.Fproduct_Tm_refine_309bd01ae86f04be15be0d04630f43d6",
"refinement_interpretation_Hacl.Spec.Bignum.Fproduct_Tm_refine_8b47bbebde5573924fb09f9ea16c86c8",
"refinement_interpretation_Hacl.Spec.Bignum.Fproduct_Tm_refine_b1de792120be2aa87d7f0324511b3651",
"refinement_interpretation_Hacl.Spec.Bignum.Fproduct_Tm_refine_dacebda014c945d52a146fae3cbf6b0a",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_6dc45e0b5fcbd0cd9230c5e1d2129995",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_93e478e51afb551fb2b3a237a56e1775",
"refinement_interpretation_Hacl.Spec.Bignum.Fsquare_Tm_refine_da652ff6088989bf00b630ff6a607821",
"refinement_interpretation_Hacl.Spec.Bignum.Modulo_Tm_refine_74884dd4ddb6983904977c02f676a9fc",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_51400a2963b1a03190be41ae7973a8a2",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Spec.Loops_Tm_refine_b5e6bf0afe978ce3dd595c1a3a4a6fae",
"token_correspondence_Hacl.Bignum.Parameters.wide_to_limb",
"typing_Hacl.Spec.Bignum.Fproduct.carry_0_to_1_spec",
"typing_Hacl.Spec.Bignum.Fproduct.carry_wide_spec",
"typing_Hacl.Spec.Bignum.Fsquare.fsquare_spec_",
"typing_Hacl.Spec.Bignum.Modulo.carry_top_wide_spec",
"typing_Spec.Loops.seq_map"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_fsquare_times",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_fsquare_times",
2,
0,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.Bignum.Fsquare.fsquare_times_tot.fuel_instrumented",
"@query", "binder_x_81c027918bb49ea621b89a03793896cc_0",
"binder_x_cda60864cf6228d7a4fba58b6264c802_1",
"binder_x_cda60864cf6228d7a4fba58b6264c802_2",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Monotonic.HyperHeap.test0",
"equation_FStar.UInt.min_int",
"equation_Hacl.Bignum.Parameters.seqelem", "equation_Prims._assert",
"equation_Prims.pos",
"function_token_typing_FStar.Monotonic.HyperHeap.test0",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Hacl.Spec.EC.AddAndDouble_Tm_refine_8ed80e5754ec40c80bc8e499121644eb",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Hacl.Spec.Bignum.Fsquare.fsquare_times_tot",
"well-founded-ordering-on-nat"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_fsquare_times",
3,
0,
0,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times_",
1,
1,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times_",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.buffer",
"equation_FStar.UInt32.t", "equation_FStar.UInt64.t",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Parameters.felem",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_484a6e6064fc1ae01de63e2e98020bbf",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times_",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "eq2-interp",
"equation_FStar.Buffer.buffer", "equation_FStar.Buffer.live",
"equation_FStar.Monotonic.HyperHeap.contains_ref",
"equation_FStar.Monotonic.HyperStack.contains",
"equation_FStar.UInt.fits", "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.n", "equation_FStar.UInt64.t",
"equation_FStar.UInt64.uint_to_t",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.wide",
"equation_Hacl.Bignum.Constants.word_size",
"equation_Hacl.Bignum.Parameters.felem",
"equation_Hacl.Bignum.Parameters.felem_wide",
"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.wide",
"equation_Hacl.Bignum.Parameters.word_size",
"equation_Hacl.Cast.uint64_to_sint64",
"equation_Hacl.Spec.Bignum.Fsquare.fsquare_pre",
"equation_Hacl.Spec.Bignum.Modulo.carry_top_wide_pre",
"equation_Hacl.Spec.EC.AddAndDouble.red_513",
"equation_Hacl.UInt128.t",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
"fuel_guarded_inversion_FStar.UInt32.t_",
"function_token_typing_Hacl.Bignum.Parameters.limb_one",
"function_token_typing_Hacl.UInt128.t",
"interpretation_Hacl.Bignum.Fsquare_Tm_abs_807b31abb760e8e03e9c8c8aa327966c",
"kinding_FStar.UInt64.t_@tok", "l_and-interp",
"lemma_FStar.Buffer.lemma_disjoint_symm",
"lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_FStar.Monotonic.HyperStack.HS_h",
"proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt32.Mk_v",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_484a6e6064fc1ae01de63e2e98020bbf",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_a75449b7b5f24c622e068f573fc2b030",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_c8bc8082cc1e965c8824145787ef46bb",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_b6cddb0925a26b22bc7c5884d275beb2",
"typing_FStar.Buffer.as_seq", "typing_Hacl.Bignum.Parameters.v"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times_",
4,
0,
0,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times",
1,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.buffer",
"equation_FStar.UInt32.t", "equation_FStar.UInt64.t",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Parameters.felem",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_484a6e6064fc1ae01de63e2e98020bbf",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Monotonic.HyperHeap.HasEq_rid", "bool_inversion",
"data_elim_FStar.Monotonic.HyperStack.HS",
"data_elim_FStar.Monotonic.HyperStack.MkRef", "eq2-interp",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.content", "equation_FStar.Buffer.equal",
"equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.idx",
"equation_FStar.Buffer.live",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.HyperStack.reference",
"equation_FStar.Monotonic.HyperHeap.t",
"equation_FStar.Monotonic.HyperStack.contains",
"equation_FStar.Monotonic.HyperStack.equal_domains",
"equation_FStar.Monotonic.HyperStack.frameOf",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.hh",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.live_region",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.Set.eqtype", "equation_FStar.UInt32.t",
"equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v",
"equation_FStar.UInt64.t", "equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.wide",
"equation_Hacl.Bignum.Parameters.clen",
"equation_Hacl.Bignum.Parameters.felem",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.wide", "equation_Hacl.UInt128.t",
"equation_Prims.eqtype",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
"fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference",
"fuel_guarded_inversion_FStar.UInt32.t_",
"function_token_typing_FStar.Monotonic.Heap.emp",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.Monotonic.HyperHeap.rid",
"function_token_typing_Hacl.Bignum.Parameters.clen",
"function_token_typing_Hacl.UInt128.t",
"kinding_FStar.UInt64.t_@tok",
"lemma_FStar.Buffer.lemma_disjoint_symm",
"lemma_FStar.Buffer.lemma_equal_domains_2",
"lemma_FStar.Buffer.lemma_fresh_poppable",
"lemma_FStar.Buffer.lemma_live_disjoint",
"lemma_FStar.Buffer.lemma_modifies_0_2_",
"lemma_FStar.Buffer.lemma_modifies_1_2___",
"lemma_FStar.Buffer.lemma_modifies_2_comm",
"lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped",
"lemma_FStar.Buffer.modifies_poppable_0",
"lemma_FStar.Buffer.modifies_poppable_1",
"lemma_FStar.Buffer.modifies_poppable_2",
"lemma_FStar.Buffer.modifies_popped_1",
"lemma_FStar.Buffer.no_upd_fresh",
"lemma_FStar.Buffer.no_upd_lemma_0",
"lemma_FStar.Buffer.no_upd_lemma_1",
"lemma_FStar.Buffer.no_upd_popped",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1",
"lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans",
"lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement",
"lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_Negation", "primitive_Prims.op_disEquality",
"proj_equation_FStar.Buffer.MkBuffer_content",
"proj_equation_FStar.Buffer.MkBuffer_idx",
"proj_equation_FStar.Monotonic.HyperStack.HS_h",
"proj_equation_FStar.Monotonic.HyperStack.HS_tip",
"proj_equation_FStar.Monotonic.HyperStack.MkRef_id",
"proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Monotonic.HyperStack.HS_h",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_0418702750d54a72833a38f310956e3d",
"refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_38d52172626ad62ce3b0e4245dab71ed",
"refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_b05295ea25e1fbfe5a4bd48cb81ddfff",
"refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882",
"refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_FStar.Buffer.__proj__MkBuffer__item__content",
"typing_FStar.Buffer.__proj__MkBuffer__item__idx",
"typing_FStar.Buffer.as_seq", "typing_FStar.Map.contains",
"typing_FStar.Map.domain",
"typing_FStar.Monotonic.HyperStack.__proj__HS__item__h",
"typing_FStar.Monotonic.HyperStack.__proj__HS__item__tip",
"typing_FStar.Monotonic.HyperStack.poppable",
"typing_FStar.Set.complement", "typing_FStar.Set.intersect",
"typing_FStar.Set.singleton"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times_inplace",
1,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times_inplace",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.buffer",
"equation_FStar.UInt32.t", "equation_FStar.UInt64.t",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Parameters.felem",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_Hacl.Bignum.Fsquare_Tm_refine_484a6e6064fc1ae01de63e2e98020bbf",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882"
],
0
],
[
"Hacl.Bignum.Fsquare.fsquare_times_inplace",
3,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.Bignum.Fsquare.fsquare_times_tot.fuel_instrumented",
"@query", "assumption_FStar.Monotonic.HyperHeap.HasEq_rid",
"bool_inversion", "data_elim_FStar.Monotonic.HyperStack.HS",
"data_elim_FStar.Monotonic.HyperStack.MkRef", "eq2-interp",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.content", "equation_FStar.Buffer.equal",
"equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.live",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.HyperStack.reference",
"equation_FStar.Monotonic.HyperHeap.t",
"equation_FStar.Monotonic.HyperStack.contains",
"equation_FStar.Monotonic.HyperStack.equal_domains",
"equation_FStar.Monotonic.HyperStack.frameOf",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.hh",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.live_region",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.Set.eqtype", "equation_FStar.UInt32.t",
"equation_FStar.UInt32.v", "equation_FStar.UInt64.t",
"equation_Hacl.Bignum.Constants.len",
"equation_Hacl.Bignum.Constants.limb",
"equation_Hacl.Bignum.Constants.wide",
"equation_Hacl.Bignum.Parameters.clen",
"equation_Hacl.Bignum.Parameters.felem",
"equation_Hacl.Bignum.Parameters.len",
"equation_Hacl.Bignum.Parameters.limb",
"equation_Hacl.Bignum.Parameters.wide", "equation_Hacl.UInt128.t",
"equation_Prims.eqtype",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
"fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference",
"function_token_typing_FStar.Monotonic.Heap.emp",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_FStar.Monotonic.HyperHeap.rid",
"function_token_typing_Hacl.Bignum.Parameters.clen",
"function_token_typing_Hacl.UInt128.t",
"kinding_FStar.UInt64.t_@tok",
"lemma_FStar.Buffer.lemma_equal_domains_2",
"lemma_FStar.Buffer.lemma_fresh_poppable",
"lemma_FStar.Buffer.lemma_live_disjoint",
"lemma_FStar.Buffer.lemma_modifies_0_2",
"lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped",
"lemma_FStar.Buffer.modifies_poppable_0",
"lemma_FStar.Buffer.modifies_poppable_2",
"lemma_FStar.Buffer.modifies_popped_1",
"lemma_FStar.Buffer.no_upd_fresh",
"lemma_FStar.Buffer.no_upd_lemma_0",
"lemma_FStar.Buffer.no_upd_popped",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1",
"lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement",
"lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_Negation",
"primitive_Prims.op_disEquality",
"proj_equation_FStar.Buffer.MkBuffer_content",
"proj_equation_FStar.Monotonic.HyperStack.HS_h",
"proj_equation_FStar.Monotonic.HyperStack.HS_tip",
"proj_equation_FStar.Monotonic.HyperStack.MkRef_id",
"proj_equation_FStar.Monotonic.HyperStack.MkRef_ref",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Monotonic.HyperStack.HS_h",
"refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_0418702750d54a72833a38f310956e3d",
"refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_38d52172626ad62ce3b0e4245dab71ed",
"refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_b05295ea25e1fbfe5a4bd48cb81ddfff",
"refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Hacl.Bignum.Parameters_Tm_refine_2cce8b21947d7cc0465fdc87c7a1f882",
"refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_FStar.Buffer.__proj__MkBuffer__item__content",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Monotonic.HyperStack.__proj__HS__item__h",
"typing_FStar.Monotonic.HyperStack.__proj__HS__item__tip",
"typing_FStar.Monotonic.HyperStack.poppable",
"typing_FStar.Set.complement", "typing_FStar.Set.intersect",
"typing_FStar.Set.singleton"
],
0
]
]
]