Revision 9c7444102374d3650ce16ea2cf8d6b8a726dd2df authored by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC, committed by Victor Dumitrescu on 11 May 2020, 16:25:39 UTC
1 parent 6cadaf2
Hacl.Spec.P256.Lemmas.fst.hints
[
"�ދ��w\u0016��E��ylQr",
[
[
"Hacl.Spec.P256.Lemmas.pow",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"8292cd43015c03784fa5313943943d30"
],
[
"Hacl.Spec.P256.Lemmas.modulo_distributivity_mult",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"a6f130999d5a0f96502d64baca0f0e5a"
],
[
"Hacl.Spec.P256.Lemmas.modulo_distributivity_mult",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"379c8b29364e9dfc98f2b19f7541b9a1"
],
[
"Hacl.Spec.P256.Lemmas.power_one",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@query", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"equation_Prims.nat",
"equation_with_fuel_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"int_inversion", "int_typing", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"well-founded-ordering-on-nat"
],
0,
"db5ef465c30609c525c7bea06e7f2b24"
],
[
"Hacl.Spec.P256.Lemmas.pow_plus",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"d8fcc9a794b259f9e506c748beeb3ca0"
],
[
"Hacl.Spec.P256.Lemmas.pow_plus",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b9402129eb7df5a3ac93582c3e759735"
],
0,
"1c6a6d35b5461db0bc4ab9a32ce62d19"
],
[
"Hacl.Spec.P256.Lemmas.pow_plus",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Prims.LexTop@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_with_fuel_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Hacl.Spec.P256.Lemmas.pow", "well-founded-ordering-on-nat"
],
0,
"8395d3257acd655f12a5115c75fc406c"
],
[
"Hacl.Spec.P256.Lemmas.power_distributivity",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"609122581d1009061072d046ecdbf09f"
],
[
"Hacl.Spec.P256.Lemmas.power_distributivity",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_bdeb6db01cb210f3d8065fe9f1aed84e"
],
0,
"cedc32cff6a9079ec132b9e2e1f738cc"
],
[
"Hacl.Spec.P256.Lemmas.power_distributivity",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_2",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"well-founded-ordering-on-nat"
],
0,
"3a3890f98a1792e735855d30592078be"
],
[
"Hacl.Spec.P256.Lemmas.power_distributivity_2",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"6bc3c86d0118f39186367f8609a92543"
],
[
"Hacl.Spec.P256.Lemmas.power_distributivity_2",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_fd86cf7119ab5e0fc5d19760497f4fb4"
],
0,
"34eb472bd741dcbdfb68703a98075759"
],
[
"Hacl.Spec.P256.Lemmas.power_distributivity_2",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"true_interp", "typing_Hacl.Spec.P256.Lemmas.pow",
"well-founded-ordering-on-nat"
],
0,
"877d20271b9a14b33008bfc16f95e2e1"
],
[
"Hacl.Spec.P256.Lemmas.power_distributivity_2",
4,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_2",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_062cbd0c97c909c6d4130dd670a90407",
"refinement_interpretation_Tm_refine_2c64c9673238307efb67bd6b160253bb",
"refinement_interpretation_Tm_refine_2d108d64e0cd3a598f2f1f509a6f285d",
"refinement_interpretation_Tm_refine_38db2b09bb8b89aeed5dd0248b629e5a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_69b2710bb02324b17931ddf6fed00446",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7baf7734c0499a0a02e6d4e69a16dde2",
"refinement_interpretation_Tm_refine_7f9805659f4f02197b3577bb3fdcbee5",
"refinement_interpretation_Tm_refine_a99b12586ec20bf9af5d8f87595dfdff",
"refinement_interpretation_Tm_refine_b349053791df39c359d480bf4687a2ab",
"refinement_interpretation_Tm_refine_c4abe1da1880a2b8a49bf2959ac36884",
"refinement_interpretation_Tm_refine_fc16013fc1c7f905cd26741969ab2657",
"typing_Hacl.Spec.P256.Lemmas.pow"
],
0,
"cfcac8021bf52d6a251726825dcee1ea"
],
[
"Hacl.Spec.P256.Lemmas.power_mult",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"688367e4c0460c71df12ca6d54a5c285"
],
[
"Hacl.Spec.P256.Lemmas.power_mult",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ab1298ae9c797babb0ad7c78eaa15ff5"
],
0,
"b1d67c2f4b9edd8d7b33d06036830e51"
],
[
"Hacl.Spec.P256.Lemmas.power_mult",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Prims.LexTop@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_with_fuel_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_bcf1e30f90c38989866b12321115ea81",
"token_correspondence_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"typing_Hacl.Spec.P256.Lemmas.pow", "well-founded-ordering-on-nat"
],
0,
"d584bd9a3e2cc4089e05fe694b21026d"
],
[
"Hacl.Spec.P256.Lemmas.log_and",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"a7522255955e9802aaaae5f8ad04f474"
],
[
"Hacl.Spec.P256.Lemmas.log_and",
2,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"046ecbef2edcc40d2bc9df123cb915b0"
],
[
"Hacl.Spec.P256.Lemmas.log_and",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.logand_v", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.ones_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v",
"function_token_typing_Prims.__cache_version_number__",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_ea00864f59112084603b9e9c26fa7914",
"typing_Lib.IntTypes.logand_v", "typing_Lib.IntTypes.v",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"dafff37b4a9936a08930113c9b0ca89b"
],
[
"Hacl.Spec.P256.Lemmas.logor_commutative",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.logor_v", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"typing_Lib.IntTypes.logor", "typing_Lib.IntTypes.v",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"7c4a16926e2226d0a969dd7167f217c0"
],
[
"Hacl.Spec.P256.Lemmas.log_or",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"1c905c48545e383d2246c9ce389b1587"
],
[
"Hacl.Spec.P256.Lemmas.log_or",
2,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"5123b58f7e3e30a0e5b03b2ecf0711f2"
],
[
"Hacl.Spec.P256.Lemmas.log_or",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3336c263a8f81f44fe63e11e8a94ae99",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"e41142a5916c9a52681cf3ec466dd24b"
],
[
"Hacl.Spec.P256.Lemmas.fmul",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"69223316ececc96e60215120a9b55af0"
],
[
"Hacl.Spec.P256.Lemmas.exp",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"well-founded-ordering-on-nat"
],
0,
"87b75c3d94ae4511f1bf87a83fb17681"
],
[
"Hacl.Spec.P256.Lemmas.modp_inv_prime",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_fd0d082075d797d9d29faee2f7221b9b"
],
0,
"400f27316afa0b433ea255bffdadc3fb"
],
[
"Hacl.Spec.P256.Lemmas.modp_inv2_prime",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_252208e03527988c441dcde8cef45502",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"af968399e4c6c3fda3082f49570d4013"
],
[
"Hacl.Spec.P256.Lemmas.modp_inv2",
1,
4,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Hacl.Spec.P256.Definitions.prime256",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Prims.pow2"
],
0,
"9bd94f262740312006d837c57fdcb2bd"
],
[
"Hacl.Spec.P256.Lemmas.modp_inv2_pow",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Hacl.Spec.P256.Definitions.prime256",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Hacl.Spec.P256.Definitions.prime256"
],
0,
"de4f986bc5b918d18436bd1be4b70b6e"
],
[
"Hacl.Spec.P256.Lemmas.min_one_prime",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_fd0d082075d797d9d29faee2f7221b9b"
],
0,
"3bc6a49192a4f7b0223239ab8cd655e4"
],
[
"Hacl.Spec.P256.Lemmas.lemma_fpow_unfold0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.P256.Lemmas.elem", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1da93ef63852a3a506544a292b2657a4",
"refinement_interpretation_Tm_refine_39df8d29380e6969edd244cad5059985",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"af893bede9dfeaf670b4d779f6a28bec"
],
[
"Hacl.Spec.P256.Lemmas.lemma_fpow_unfold0",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.P256.Lemmas.exp.fuel_instrumented",
"@fuel_irrelevance_Hacl.Spec.P256.Lemmas.exp.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Hacl.Spec.P256.Lemmas.elem",
"equation_Hacl.Spec.P256.Lemmas.fmul", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Hacl.Spec.P256.Lemmas.exp.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_1da93ef63852a3a506544a292b2657a4",
"refinement_interpretation_Tm_refine_39df8d29380e6969edd244cad5059985",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"9d69768fb62c7db85653964a79b173fe"
],
[
"Hacl.Spec.P256.Lemmas.lemma_fpow_unfold1",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.P256.Lemmas.elem", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "int_inversion",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_39df8d29380e6969edd244cad5059985",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5c810aa3d09a59fa0969eff7c23d634f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"c6d0f8bd36b9def22320f1146ee6d3c6"
],
[
"Hacl.Spec.P256.Lemmas.lemma_fpow_unfold1",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.P256.Lemmas.exp.fuel_instrumented",
"@fuel_irrelevance_Hacl.Spec.P256.Lemmas.exp.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Hacl.Spec.P256.Lemmas.elem",
"equation_Hacl.Spec.P256.Lemmas.fmul",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Hacl.Spec.P256.Lemmas.exp.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_39df8d29380e6969edd244cad5059985",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5c810aa3d09a59fa0969eff7c23d634f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Hacl.Spec.P256.Lemmas.exp",
"typing_Hacl.Spec.P256.Lemmas.fmul"
],
0,
"327feba9357ae5a335d40294c5d593fd"
],
[
"Hacl.Spec.P256.Lemmas.lemma_pow_unfold",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"56d1367b851e6557234331c2c448e0e7"
],
[
"Hacl.Spec.P256.Lemmas.lemma_pow_unfold",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Equality",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"c36c53fe6a90cdc34c2d1a2662eb0be0"
],
[
"Hacl.Spec.P256.Lemmas.lemma_mul_ass3",
1,
2,
1,
[
"@query", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0"
],
0,
"b10469480d48496529e01d8aafb3ecdd"
],
[
"Hacl.Spec.P256.Lemmas.lemma_pow_double",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"8157e107f54ea56abbe84937ec5f1b27"
],
[
"Hacl.Spec.P256.Lemmas.lemma_pow_double",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_53bd873aa62dd4bba37f91a10f5a429a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"e9b3a4ba954fb6ac5ad74dec0aecc87f"
],
[
"Hacl.Spec.P256.Lemmas.lemma_pow_double",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Prims.LexTop@tok",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat",
"equation_with_fuel_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"typing_Hacl.Spec.P256.Lemmas.pow", "typing_Lib.IntTypes.minint",
"typing_tok_Lib.IntTypes.U32@tok", "well-founded-ordering-on-nat"
],
0,
"8d0c87184fde20f0b1678eb0d27711fc"
],
[
"Hacl.Spec.P256.Lemmas.lemma_pow_mod_n_is_fpow",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"0698b204f60078c6ca344f1f7827bc52"
],
[
"Hacl.Spec.P256.Lemmas.lemma_pow_mod_n_is_fpow",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_d5f0169927ad1425a4dd42444b056f37"
],
0,
"0c81428f796658b3ddbe83371379f1f4"
],
[
"Hacl.Spec.P256.Lemmas.lemma_pow_mod_n_is_fpow",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Hacl.Spec.P256.Lemmas.exp.fuel_instrumented",
"@fuel_correspondence_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_a6ca6afaf28feca12f50f23fc064a6db_1",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_2",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Prims.LexTop@tok",
"equation_Hacl.Spec.P256.Lemmas.elem",
"equation_Hacl.Spec.P256.Lemmas.fmul",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Hacl.Spec.P256.Lemmas.exp.fuel_instrumented",
"equation_with_fuel_Hacl.Spec.P256.Lemmas.pow.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_f61c88f7b091b2f36e8249b0c1c7337c",
"typing_Hacl.Spec.P256.Lemmas.pow", "typing_Lib.IntTypes.minint",
"typing_tok_Lib.IntTypes.U32@tok", "unit_inversion", "unit_typing",
"well-founded-ordering-on-nat"
],
0,
"3742e975cacbf54d3217f5eaf92deaeb"
],
[
"Hacl.Spec.P256.Lemmas.modulo_distributivity_mult_last_two",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"eb0dc2ed7f47ffa8b3df4dc66caa933e"
],
[
"Hacl.Spec.P256.Lemmas.modulo_distributivity_mult_last_two",
2,
2,
1,
[ "@query", "true_interp" ],
0,
"80526ec7486ab3049aec4863dc88587f"
],
[
"Hacl.Spec.P256.Lemmas.lemma_mod_twice",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"8a9ed2f99eb2fa5c549b7792ce3a202f"
],
[
"Hacl.Spec.P256.Lemmas.lemma_mod_twice",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"a76ad8405d843e4935854dc1cd93b289"
],
[
"Hacl.Spec.P256.Lemmas.lemma_multiplication_to_same_number",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"0f890e966f3e648b4c1886a0fcdeede7"
],
[
"Hacl.Spec.P256.Lemmas.lemma_multiplication_to_same_number",
2,
2,
1,
[ "@query" ],
0,
"3c68a641831b38d7cdc5e38baf83946a"
],
[
"Hacl.Spec.P256.Lemmas.lemma_division_is_multiplication",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.pos", "function_token_typing_Prims.int",
"haseqTm_refine_774ba3f728d91ead8ef40be66c9802e5",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_b4b0e381c5cc374bca9911856b10ee99"
],
0,
"b231683983a448d44ab6207728bbc50c"
],
[
"Hacl.Spec.P256.Lemmas.lemma_division_is_multiplication",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.pos", "function_token_typing_Prims.int",
"haseqTm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"ace2b92e90397677dcc9459e09a37c27"
],
[
"Hacl.Spec.P256.Lemmas.lemma_division_is_multiplication",
3,
4,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Hacl.Spec.P256.Definitions.prime256",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Prims.nonzero", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
"refinement_interpretation_Tm_refine_b4b0e381c5cc374bca9911856b10ee99",
"refinement_interpretation_Tm_refine_fed8536021b958a65a4892b081fd8059",
"token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
"typing_Prims.pow2"
],
0,
"8bd01f617111136b0af98bb40a5463a3"
],
[
"Hacl.Spec.P256.Lemmas.lemma_reduce_mod_by_sub3",
1,
2,
1,
[ "@query" ],
0,
"8ba3b44d9152cfa9f68cd0d769328a78"
],
[
"Hacl.Spec.P256.Lemmas.lemma_reduce_mod_by_sub3",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Hacl.Spec.P256.Definitions.prime256",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Prims.pow2"
],
0,
"b6050635850d85386205ed89b8f88a9a"
],
[
"Hacl.Spec.P256.Lemmas.mult_one_round",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.P256.Definitions.prime256",
"equation_Prims.nonzero", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
"typing_Hacl.Spec.P256.Definitions.prime256"
],
0,
"c52900d22a0212cba5c37eee1bae3bbd"
],
[
"Hacl.Spec.P256.Lemmas.mult_one_round",
2,
2,
1,
[ "@query" ],
0,
"04237a801e9bb1b0750ec4fb6694c1d2"
],
[
"Hacl.Spec.P256.Lemmas.mult_one_round",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Hacl.Spec.P256.Definitions.prime256",
"equation_Hacl.Spec.P256.Lemmas.modp_inv2", "equation_Prims.nat",
"equation_Prims.nonzero", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
"refinement_interpretation_Tm_refine_ef726b67df02a5e104a26e76a5441d2e",
"typing_Hacl.Spec.P256.Definitions.prime256", "typing_Prims.pow2"
],
0,
"0524ead3031eb25369aa271d46e7822e"
],
[
"Hacl.Spec.P256.Lemmas.lemma_reduce_mod_ecdsa_prime",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Prims.pow2.fuel_instrumented"
],
0,
"f5dd521eebbc87984cbbe4e4c18d4b25"
],
[
"Hacl.Spec.P256.Lemmas.lemma_reduce_mod_ecdsa_prime",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Prims.pow2.fuel_instrumented"
],
0,
"14abaa28ea778de1ee840f523907b811"
],
[
"Hacl.Spec.P256.Lemmas.lemma_reduce_mod_ecdsa_prime",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Hacl.Spec.P256.Lemmas.min_one_prime",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Minus",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_b642ff384a51b331c7f7990febb5201c",
"refinement_interpretation_Tm_refine_cb5e5fec8e08b4b5437a6bdb94f9d19c",
"token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
"typing_Prims.pow2"
],
0,
"9ee902ff32598113bee37729c1acf7dc"
],
[
"Hacl.Spec.P256.Lemmas.mult_one_round_ecdsa_prime",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_bac5c0dbb945570f99dc5aa2dac84a6c",
"token_correspondence_Prims.pow2.fuel_instrumented"
],
0,
"7687da7c0bc2f71ffc9b4ef26c4cb9f2"
],
[
"Hacl.Spec.P256.Lemmas.mult_one_round_ecdsa_prime",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_bac5c0dbb945570f99dc5aa2dac84a6c",
"token_correspondence_Prims.pow2.fuel_instrumented"
],
0,
"bcbd4877c6b4c1457fa00d6a2cedaba2"
],
[
"Hacl.Spec.P256.Lemmas.mult_one_round_ecdsa_prime",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32", "equation_Prims.nat",
"equation_Prims.nonzero", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
"refinement_interpretation_Tm_refine_4228baa86be216e95409610b6c046207",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_bac5c0dbb945570f99dc5aa2dac84a6c",
"typing_Prims.pow2"
],
0,
"708096d17e62b3eb1010f76e015b33d8"
],
[
"Hacl.Spec.P256.Lemmas.lemma_decrease_pow",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.P256.Definitions.prime256", "equation_Prims.nat",
"equation_Prims.pos", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
"typing_Hacl.Spec.P256.Definitions.prime256"
],
0,
"0a85b48aa449fcfe2116823321c8a61e"
],
[
"Hacl.Spec.P256.Lemmas.lemma_decrease_pow",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.P256.Definitions.prime256",
"equation_Hacl.Spec.P256.Lemmas.elem", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Hacl.Spec.P256.Definitions.prime256"
],
0,
"a822e5d9cc5ba68fe20b70c69c6c5031"
],
[
"Hacl.Spec.P256.Lemmas.lemma_brackets",
1,
2,
1,
[
"@query", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0"
],
0,
"b6a01945cd09d6de68779bd5a31ac517"
],
[
"Hacl.Spec.P256.Lemmas.lemma_brackets1",
1,
2,
1,
[
"@query", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0"
],
0,
"ac55f703402f372c78b71ada668cc593"
],
[
"Hacl.Spec.P256.Lemmas.lemma_brackets5",
1,
2,
1,
[
"@query", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0"
],
0,
"159f5ff7b6de74c6155acebbdbf18d07"
],
[
"Hacl.Spec.P256.Lemmas.lemma_brackets4",
1,
2,
2,
[
"@query", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0"
],
0,
"b50491bd1bb3150d342e20c7e0644b0a"
],
[
"Hacl.Spec.P256.Lemmas.lemma_brackets5_0",
1,
2,
1,
[
"@query", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0"
],
0,
"2e5f53c627006cefd48b8f640701ee0c"
],
[
"Hacl.Spec.P256.Lemmas.lemma_brackets5_twice",
1,
2,
1,
[ "@query", "true_interp" ],
0,
"55e587dcf828830961499d313db09c4e"
],
[
"Hacl.Spec.P256.Lemmas.lemma_distr_mult",
1,
2,
1,
[
"@query", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0"
],
0,
"246c3507a6db3c8dde507b33ec4e9c28"
],
[
"Hacl.Spec.P256.Lemmas.lemma_twice_brackets",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0"
],
0,
"06118fd2d50689ba67c8f03035b5edfd"
],
[
"Hacl.Spec.P256.Lemmas.lemma_distr_mult7",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.bits", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0"
],
0,
"edb5510ebf358d876d69c1640e3c7201"
],
[
"Hacl.Spec.P256.Lemmas.lemma_prime_as_wide_nat",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"9c8a3b0755796de50030f0c9ea10aa44"
],
[
"Hacl.Spec.P256.Lemmas.lemma_prime_as_wide_nat",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Hacl.Spec.P256.Definitions.as_nat4",
"equation_Hacl.Spec.P256.Definitions.prime256",
"equation_Hacl.Spec.P256.Definitions.wide_as_nat4",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__5",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__6",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__7",
"projection_inverse_FStar.Pervasives.Native.Mktuple8__8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_64b4fe227e138721deebe23bb7eac0d7",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"typing_Hacl.Spec.P256.Definitions.prime256",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"e5c95a8a9e945226c3972fed7a2f725f"
],
[
"Hacl.Spec.P256.Lemmas.lemma_mul_nat2",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"7257fa87d83e1f1bb4c28c696e942e4a"
],
[
"Hacl.Spec.P256.Lemmas.lemma_mul_nat",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"7804ff0821e2f88e7ac74eb8d465f54f"
],
[
"Hacl.Spec.P256.Lemmas.lemma_mul_nat4",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"f972cd6e36a32583978cc62183c16e63"
],
[
"Hacl.Spec.P256.Lemmas.lemma_mul_nat5",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"3903ce07adae5dd39a29b2a209d9abd8"
],
[
"Hacl.Spec.P256.Lemmas.modulo_distributivity_mult2",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"ef9ec1e553af5bf28bb3b3110cad8430"
],
[
"Hacl.Spec.P256.Lemmas.modulo_distributivity_mult2",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.bits", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"true_interp"
],
0,
"645b9319dbaea09b611fb8ff38ad657d"
],
[
"Hacl.Spec.P256.Lemmas.lemma_minus_distr",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194"
],
0,
"4625c24e1f714ff61c2b0d8542d0cd5d"
],
[
"Hacl.Spec.P256.Lemmas.lemma_minus_distr",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Minus", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194"
],
0,
"021affe41e6fff14b069a420a8cfd4fc"
],
[
"Hacl.Spec.P256.Lemmas.lemma_mod_sub_distr",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"b351396b5bdfdebc0c58a071ec6f96b1"
],
[
"Hacl.Spec.P256.Lemmas.lemma_mod_sub_distr",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.bits", "equation_Prims.pos", "int_inversion",
"int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Minus",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"160cefa3fd5912e0b403450352a4c12b"
],
[
"Hacl.Spec.P256.Lemmas.lemma_mod_add_distr",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"3afaee42f6e8cc4fb2db61ac2062389b"
],
[
"Hacl.Spec.P256.Lemmas.lemma_mod_add_distr",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"f138d1e2cacdc89efba87f41344d3533"
],
[
"Hacl.Spec.P256.Lemmas.lemma_xor_copy_cond",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"f60683cf8ee2d8625742adc0ab89f853"
],
[
"Hacl.Spec.P256.Lemmas.lemma_xor_copy_cond",
2,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"e8e923e7f446b1a5ec1e933000f3ef29"
],
[
"Hacl.Spec.P256.Lemmas.lemma_xor_copy_cond",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Lib.IntTypes.logand",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_Lib.IntTypes.v_injective",
"primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_ea00864f59112084603b9e9c26fa7914",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.logxor",
"typing_Lib.IntTypes.v", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"d1c16f084298d7c47441434fee69a0a1"
],
[
"Hacl.Spec.P256.Lemmas.lemma_equality",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"53a0fd697b9bbde98ffc501851be11dc"
],
[
"Hacl.Spec.P256.Lemmas.lemma_equality",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"data_elim_FStar.Pervasives.Native.Mktuple4",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Hacl.Spec.P256.Definitions.as_nat4",
"equation_Hacl.Spec.P256.Definitions.felem4",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple4",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.v_injective", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"1cbcfc48242c12342d1784511890518b"
],
[
"Hacl.Spec.P256.Lemmas.cmovznz4_lemma",
1,
2,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U64",
"disc_equation_Lib.IntTypes.S128",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"2b81095509034a8d123385270d14e044"
],
[
"Hacl.Spec.P256.Lemmas.cmovznz4_lemma",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U64",
"disc_equation_Lib.IntTypes.S128",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"efcca688f3f4bd37d0d15795ecd11075"
],
[
"Hacl.Spec.P256.Lemmas.lemma_equ_felem",
1,
2,
1,
[ "@query" ],
0,
"d7ae602f92d68f934882664b1e430698"
],
[
"Hacl.Spec.P256.Lemmas.lemma_equ_felem",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44e3072b9092bb154322910bbcdd4933",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"1839e1004f5a5d0c51d1486af0d39dda"
],
[
"Hacl.Spec.P256.Lemmas.lemma_eq_funct",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Hacl.Spec.P256.Definitions.felem_seq",
"equation_Hacl.Spec.P256.Definitions.felem_seq_as_nat",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Lib.IntTypes.uint64", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.v_injective", "lemma_Lib.Sequence.eq_elim",
"lemma_Lib.Sequence.eq_intro", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0468cf865cb6d2adfc0caa5a9a84a72f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_94d5423c5f05a142222702ddebf823d8",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_b55fedf3f6e35df8876f389c2d7dd25b",
"refinement_interpretation_Tm_refine_bf5db0d59c861d6153cc34acabb8a9c8",
"refinement_interpretation_Tm_refine_cf1111b7ebc265bdd1e1455218e89a8d",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"02bdc615cd1d07b4f0eb49170d7249f1"
],
[
"Hacl.Spec.P256.Lemmas.lemma_eq_funct_",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"444e1fd8c613e27b7487adef4b4857f8"
],
[
"Hacl.Spec.P256.Lemmas.lemma_eq_funct_",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"0d6ed5d41f39bdee62c798c4597e2d26"
],
[
"Hacl.Spec.P256.Lemmas.mul_lemma_1",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"72a597e814dbe370cedaf927eb578c98"
],
[
"Hacl.Spec.P256.Lemmas.mul_lemma_",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"29ed9a58b664670cf0ec70e028586dc7"
],
[
"Hacl.Spec.P256.Lemmas.mul_lemma_2",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"a850828bb9a26597feb7a8553fdd1373"
],
[
"Hacl.Spec.P256.Lemmas.mul_lemma_3",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"e2f5deed2a0cf11dccf979ce52a561c2"
],
[
"Hacl.Spec.P256.Lemmas.mul_lemma_4",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"455c7677ddd853b22fa458be8dfe6a86"
],
[
"Hacl.Spec.P256.Lemmas.dist_lemma_0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "int_inversion", "int_typing",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0"
],
0,
"76a0a2afaaeedb187a461dcafeace8d6"
],
[
"Hacl.Spec.P256.Lemmas.lemma_low_level0",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThan",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44e3072b9092bb154322910bbcdd4933",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_79782e7f9811f917de33dda3aa0e39e9",
"typing_Prims.pow2"
],
0,
"325e13f759faf1ecfcf469623e878010"
],
[
"Hacl.Spec.P256.Lemmas.lemma_ll0",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"37c2c26474aadf08db1ab1d79aabfe39"
],
[
"Hacl.Spec.P256.Lemmas.lemma_pow_signature",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_fd0d082075d797d9d29faee2f7221b9b"
],
0,
"a14824a77fe5e9210299b948a9c9b7c6"
],
[
"Hacl.Spec.P256.Lemmas.lemma_pow_signature",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_fd0d082075d797d9d29faee2f7221b9b"
],
0,
"8ce0e4ab6c767c98f7b32811d17a1812"
]
]
]
Computing file changes ...
