[
"q\\ÛÅbú%%2öBc7\u001fï\u0003",
[
[
"Spec.P256.Lemmas.pow",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "equation_Prims.nat",
"equation_Prims.op_Equals_Equals_Equals", "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,
"af76dfc3a9e15418e0c82b6d324d017e"
],
[
"Spec.P256.Lemmas.modulo_distributivity_mult",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"ca57a817ac50f80b65cd5db8db380e2e"
],
[
"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,
"39bef3f187208947b750f203fc86258d"
],
[
"Spec.P256.Lemmas.power_one",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Spec.P256.Lemmas.pow.fuel_instrumented", "@query",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "equation_Prims.nat",
"equation_with_fuel_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,
"13f152a1e147192878fce198bc2485c4"
],
[
"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,
"fe2c55c0ea2f6336a5fdbb5ff1977cb2"
],
[
"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_bf88073ff7c1ce2a77e403522edd8b54"
],
0,
"2989350c85293c9003649aabc2dd3d50"
],
[
"Spec.P256.Lemmas.pow_plus",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_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_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_Spec.P256.Lemmas.pow", "well-founded-ordering-on-nat"
],
0,
"faafe3a19d09e958e79b595d953838bf"
],
[
"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,
"03829a54db75869d519c335314a5de5e"
],
[
"Spec.P256.Lemmas.power_distributivity",
2,
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_5df93ab5ea3eec4b0808d20e1ba85356",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"34e59ea1da7bddee71957ae89e56dfc3"
],
[
"Spec.P256.Lemmas.power_distributivity",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Spec.P256.Lemmas.pow.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_2", "equation_Prims.nat",
"equation_Prims.op_Equals_Equals_Equals", "equation_Prims.pos",
"equation_with_fuel_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,
"4871ad7d83a8db91b5555876f6f9c677"
],
[
"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,
"27ec750fdd351625f744f358eb144d47"
],
[
"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_912bd7f8dee3370862e5e94a67b3ec2a"
],
0,
"beeb1746205198a979152c2d70b1582d"
],
[
"Spec.P256.Lemmas.power_distributivity_2",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Spec.P256.Lemmas.pow.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_2", "equation_Prims.nat",
"equation_Prims.op_Equals_Equals_Equals", "equation_Prims.pos",
"equation_with_fuel_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_Spec.P256.Lemmas.pow",
"well-founded-ordering-on-nat"
],
0,
"98388cda4843ac253da4f6eb1df91125"
],
[
"Spec.P256.Lemmas.power_distributivity_2",
4,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_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.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_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_0a96d41f90294369d338ca83653523e1",
"refinement_interpretation_Tm_refine_114cc52c9ab7584f4570308345e5a544",
"refinement_interpretation_Tm_refine_1847e3fff5cf3c0ce9f56e3d8d6fd5c9",
"refinement_interpretation_Tm_refine_1932fac26c9b413deb22c4b4b67f6503",
"refinement_interpretation_Tm_refine_38db2b09bb8b89aeed5dd0248b629e5a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_69b2710bb02324b17931ddf6fed00446",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_998f437f6fb067769ac43d8153641b7c",
"refinement_interpretation_Tm_refine_a84f2791afb750ee158ca6b7500db79b",
"refinement_interpretation_Tm_refine_ba4856292e5dcdd4aa3f3cdd1ad179eb",
"refinement_interpretation_Tm_refine_cb71def8170a6e37199328b7a919784a",
"refinement_interpretation_Tm_refine_d944468013a9f9c1e8aa0d15bcae4709",
"refinement_interpretation_Tm_refine_f788ebdfc5d29b9cd0aabbe180425da7"
],
0,
"1aaca51ac314e67926d68a51061aff2b"
],
[
"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,
"443b2619b4ab16f6ae6671fe5aaef739"
],
[
"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_90c3a80846945672a3f0f5de29127d97"
],
0,
"c23bbcb3a84379bda260f25720c4fd1e"
],
[
"Spec.P256.Lemmas.power_mult",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Spec.P256.Lemmas.pow.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "equation_Prims.nat",
"equation_Prims.op_Equals_Equals_Equals",
"equation_with_fuel_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_Spec.P256.Lemmas.pow", "well-founded-ordering-on-nat"
],
0,
"c77a2352f09bd8b42773f95fca1db621"
],
[
"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,
"cc459589087cf31dc24884d3be0c4d54"
],
[
"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,
"1e65600358aa52a2b49b3a509744d3cf"
],
[
"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,
"c40b09fd45ffca1c653a5c8f8d002b83"
],
[
"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,
"89b9a4bf3a14cf308305285f56585771"
],
[
"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,
"4b30770f54d0720ce1aae6d541b9caeb"
],
[
"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,
"35a58f40bab833a0032c239f02a32527"
],
[
"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,
"2680c4794fb6ab57f1625a74a94f6029"
],
[
"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,
"25c1d367fd88ca495ab4ecdf8832e6e9"
],
[
"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,
"b06cec42450cae474ba9a7981437c413"
],
[
"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,
"af47fbfa19411d82e3a249aa0a36888a"
],
[
"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,
"a1c92fc1f176a05b7ee398ea23c41192"
],
[
"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_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.P256.Definitions.prime256",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"57107654b7e8b362f6224f77c6bb45bb"
],
[
"Spec.P256.Lemmas.modp_inv2_pow",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_Spec.P256.Definitions.prime256",
"primitive_Prims.op_GreaterThan", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
"typing_Spec.P256.Definitions.prime256"
],
0,
"0b33ee858fbc67f41531d3422d885f37"
],
[
"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,
"e832de4a071a8ae8fe1bc132194066f3"
],
[
"Spec.P256.Lemmas.lemma_fpow_unfold0",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.P256.Lemmas.elem", "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,
"1a82453a602792c324779218b11c0f88"
],
[
"Spec.P256.Lemmas.lemma_fpow_unfold0",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.P256.Lemmas.exp.fuel_instrumented",
"@fuel_irrelevance_Spec.P256.Lemmas.exp.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.P256.Lemmas.elem", "equation_Spec.P256.Lemmas.fmul",
"equation_with_fuel_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,
"ed28e3e8653c67f20644de27365c4bb2"
],
[
"Spec.P256.Lemmas.lemma_fpow_unfold1",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.P256.Lemmas.elem", "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,
"b8aed322e2d6d4f6e41483a49a60fc44"
],
[
"Spec.P256.Lemmas.lemma_fpow_unfold1",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.P256.Lemmas.exp.fuel_instrumented",
"@fuel_irrelevance_Spec.P256.Lemmas.exp.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.P256.Lemmas.elem", "equation_Spec.P256.Lemmas.fmul",
"equation_with_fuel_Spec.P256.Lemmas.exp.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "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"
],
0,
"94ecf9af55ce9a6385b64efbca53fd2e"
],
[
"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,
"428ce7a158960108977ef79d934d582f"
],
[
"Spec.P256.Lemmas.lemma_pow_unfold",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Spec.P256.Lemmas.pow.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_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,
"bab2e0aaa258794c62d13082bd5e1330"
],
[
"Spec.P256.Lemmas.lemma_mul_associativity_3",
1,
2,
1,
[
"@query", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0"
],
0,
"f8ccf183f104299ff89524d40eba2524"
],
[
"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,
"6c21ef705eec34b76f1383f6fcc09e59"
],
[
"Spec.P256.Lemmas.lemma_pow_double",
2,
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",
"refinement_interpretation_Tm_refine_c1452bce178f7548ada8103c10b6889e"
],
0,
"5c1eeec3ab1924aa67c9678f95e17ba8"
],
[
"Spec.P256.Lemmas.lemma_pow_double",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_Spec.P256.Lemmas.pow.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "equation_Prims.nat",
"equation_Prims.op_Equals_Equals_Equals",
"equation_with_fuel_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_Spec.P256.Lemmas.pow.fuel_instrumented",
"typing_Spec.P256.Lemmas.pow", "well-founded-ordering-on-nat"
],
0,
"61bda3caf97974e7d57e7a4c5e910ca2"
],
[
"Spec.P256.Lemmas.lemma_pow_mod_n_is_fpow",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"5ad7b0ffe5e9d7bae57388c19951684d"
],
[
"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_fde648da634d897e06a9e29c55c7fb64"
],
0,
"9e3cb7107b1bd87be228d2c69aab0d46"
],
[
"Spec.P256.Lemmas.lemma_pow_mod_n_is_fpow",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.P256.Lemmas.exp.fuel_instrumented",
"@fuel_correspondence_Spec.P256.Lemmas.pow.fuel_instrumented",
"@fuel_irrelevance_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_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.P256.Lemmas.elem", "equation_Spec.P256.Lemmas.fmul",
"equation_with_fuel_Spec.P256.Lemmas.exp.fuel_instrumented",
"equation_with_fuel_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",
"token_correspondence_Spec.P256.Lemmas.pow.fuel_instrumented",
"typing_Lib.IntTypes.minint", "typing_Spec.P256.Lemmas.pow",
"typing_tok_Lib.IntTypes.U32@tok", "unit_inversion", "unit_typing",
"well-founded-ordering-on-nat"
],
0,
"46489abf5624375d410b6bca19aff8bc"
],
[
"Spec.P256.Lemmas.modulo_distributivity_mult_last_two",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"1ba7e86394a9984e3e258f9832425bc2"
],
[
"Spec.P256.Lemmas.modulo_distributivity_mult_last_two",
2,
2,
1,
[ "@query", "true_interp" ],
0,
"9f0233dcd03bf0b1546ea50ae160b74e"
],
[
"Spec.P256.Lemmas.lemma_multiplication_to_same_number",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"6debcec174e3e40ae81df71be6d0fc33"
],
[
"Spec.P256.Lemmas.lemma_multiplication_to_same_number",
2,
2,
1,
[ "@query" ],
0,
"45281ea47a3e68341a7855ed5015afbe"
],
[
"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_e602898443542ade30581f55a597ae8a"
],
0,
"fe6c281a319c578d5e38b712d2c227a3"
],
[
"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,
"bd97509abf1f026d8489b472463edd20"
],
[
"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_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Prims.nonzero", "equation_Prims.pos",
"equation_Spec.P256.Definitions.prime256",
"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_e602898443542ade30581f55a597ae8a",
"refinement_interpretation_Tm_refine_fed8536021b958a65a4892b081fd8059",
"true_interp", "typing_Prims.pow2"
],
0,
"21479053b4cdf8047b6a4bd528884159"
],
[
"Spec.P256.Lemmas.lemma_reduce_mod_by_sub3",
1,
2,
1,
[ "@query" ],
0,
"0bc000cbeb93f6ed2b7ddccfc0e660cb"
],
[
"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_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos",
"equation_Spec.P256.Definitions.prime256",
"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,
"f7a5e38f2e0ceeddea77e1908f240c75"
],
[
"Spec.P256.Lemmas.mult_one_round",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nonzero",
"equation_Prims.pos", "equation_Spec.P256.Definitions.prime256",
"refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
"typing_Spec.P256.Definitions.prime256"
],
0,
"496aa94606b3aa77b42c450b0fa8271d"
],
[
"Spec.P256.Lemmas.mult_one_round",
2,
2,
1,
[ "@query" ],
0,
"005b968e727f77ef8be5c59899885945"
],
[
"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_Prims.nat",
"equation_Prims.nonzero", "equation_Prims.pos",
"equation_Spec.P256.Definitions.prime256",
"equation_Spec.P256.Lemmas.modp_inv2", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
"refinement_interpretation_Tm_refine_0c4926e33a4dc1c024a6bb2210141ee1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_76e8779098c75b0ebe63a758ee69f13d",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Prims.pow2", "typing_Spec.P256.Definitions.prime256"
],
0,
"bb29021c3a16746339d649602299fa22"
],
[
"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,
"077f450d36d52a19fed879448470c458"
],
[
"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,
"cf30a7f95dbe961c5cde03d219165070"
],
[
"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_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos",
"equation_Spec.P256.Lemmas.min_one_prime",
"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_ff1729c3b94a65495ef3a494422da5d1",
"token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
"typing_Prims.pow2"
],
0,
"982dd916870cf491132e82c34c732456"
],
[
"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,
"ee400602c245ffe44c29bc1630c4b021"
],
[
"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,
"a208e99b1440de08d41497b9449cdc5d"
],
[
"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,
"a04bbfd317fed4219066a3fb04abd1f5"
],
[
"Spec.P256.Lemmas.lemma_decrease_pow",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.P256.Definitions.prime256",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194",
"typing_Spec.P256.Definitions.prime256"
],
0,
"5e413d9411d5cae3b7ba59bec2d3d49e"
],
[
"Spec.P256.Lemmas.lemma_decrease_pow",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Spec.P256.Definitions.prime256",
"equation_Spec.P256.Lemmas.elem", "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_Spec.P256.Definitions.prime256"
],
0,
"f3a446f9523a894375d6a6f55611ec76"
],
[
"Spec.P256.Lemmas.lemma_brackets",
1,
2,
1,
[
"@query", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0"
],
0,
"66278a9dd3f8fc5cc58d1879ad531510"
],
[
"Spec.P256.Lemmas.lemma_brackets4",
1,
2,
1,
[
"@query", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0"
],
0,
"70ce069e0fafb1d93ec68a2e2713ffe0"
],
[
"Spec.P256.Lemmas.lemma_brackets5_0",
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,
"dfe68fe7c7f53630d0c880d57f595fa2"
],
[
"Spec.P256.Lemmas.lemma_twice_brackets",
1,
2,
1,
[
"@query", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0"
],
0,
"4c57c237d446a4c28c60114579915c4d"
],
[
"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,
"e2f7b251e7b44938100d7a6b0fa5c788"
],
[
"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,
"726954b836982d7b0e7384104d43ba97"
],
[
"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,
"d4b4831450f1ff45bedc6d1a13e92ff9"
],
[
"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,
"9227156a68abeddb9c86c04f4408bbc2"
],
[
"Spec.P256.Lemmas.modulo_distributivity_mult2",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"987675c80388c8e6c21121d36f034515"
],
[
"Spec.P256.Lemmas.modulo_distributivity_mult2",
2,
2,
2,
[
"@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,
"8655b497e5b332d6d8afdc17dbfad812"
],
[
"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,
"d86eeea63d99fc4b20cbcd3601ba48cf"
],
[
"Spec.P256.Lemmas.lemma_minus_distr",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "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,
"46bce1564e9c2b5aeb200c9558288dd2"
],
[
"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,
"d92104604a444a3423585cedd309af60"
],
[
"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,
"6290705f191ce0b6b83d1baa4a596329"
],
[
"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,
"4e61d5e7f36948f61f7b72c2a570fb10"
],
[
"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,
"e418f4026f5899ad97e3a45aa5d83e26"
],
[
"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_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",
"equation_Spec.P256.Definitions.as_nat4",
"equation_Spec.P256.Definitions.felem4",
"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,
"7aa620ad0bca4cbeea488e4275c1b740"
],
[
"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,
"e739ced52c16db188533b2af50344a6d"
],
[
"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,
"76cd3f5893cce8364aefb5021c873767"
],
[
"Spec.P256.Lemmas.lemma_equ_felem",
1,
2,
1,
[ "@query" ],
0,
"cef4da8e5e45a4cfd17869cf8f65efe4"
],
[
"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",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.pow2_127", "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,
"98fefce4bd00936599554722f4db63a9"
],
[
"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_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_Spec.P256.Definitions.felem_seq",
"equation_Spec.P256.Definitions.felem_seq_as_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_2b9ac1d6c43e9e240d84837e7e466c45",
"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,
"84c4854d7537687030038ab7f10010f8"
],
[
"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,
"a17828b55919255f6230a9ddc04325a6"
],
[
"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,
"004b39a1e00f1de7c401b4469ac9d082"
],
[
"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,
"33dc23a93ac5daf0ded28d3fab47e4f7"
],
[
"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,
"80962e37e136cfe75c8d00e68e0ba16a"
],
[
"Spec.P256.Lemmas.mul_lemma_2",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"1077226b562a1873ddfe53abf404da62"
],
[
"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,
"30dc5f5ecf347c6f5565d565c99217a4"
],
[
"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,
"0ed687f153f24ffcd8afba81cb593159"
],
[
"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,
"a2e838c3da2abe72f60adecddd66aafe"
],
[
"Spec.P256.Lemmas.lemma_cswap2_step",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_f41f4015e22b272c5f61be9cc1570311",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"9e84d6a1919422870148e683fae592a7"
],
[
"Spec.P256.Lemmas.lemma_cswap2_step",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_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.U32",
"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.op_At_Percent_Dot",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Lib.IntTypes.logand",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.sub_mod_lemma", "lemma_Lib.IntTypes.v_injective",
"primitive_Prims.op_Equality", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e",
"refinement_interpretation_Tm_refine_f41f4015e22b272c5f61be9cc1570311",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.logxor",
"typing_Lib.IntTypes.maxint", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.op_At_Percent_Dot", "typing_Lib.IntTypes.v",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"4451f3404641f11c38eeec1055bef159"
]
]
]