[ "ڭ\u0015\u001f\r", [ [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.prime256order_buffer", 1, 4, 2, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.index.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.index.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion", "constructor_distinct_Lib.Buffer.CONST", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Prims.Cons", "data_elim_Prims.Cons", "equality_tok_Lib.Buffer.CONST@tok", "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.HyperStack.ST.is_eternal_region", "equation_FStar.List.Tot.Base.hd", "equation_FStar.List.Tot.Base.tail", "equation_FStar.List.Tot.Base.tl", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_heap_color", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "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_LowStar.ConstBuffer.as_mbuf", "equation_LowStar.ConstBuffer.length", "equation_LowStar.ConstBuffer.qbuf_pre", "equation_LowStar.ConstBuffer.qbuf_qual", "equation_LowStar.ConstBuffer.qual_of", "equation_Prims.nat", "equation_Spec.ECDSAP256.Definition.felem_seq_as_nat", "equation_Spec.ECDSAP256.Definition.p256_order_prime_list", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "equation_with_fuel_FStar.List.Tot.Base.index.fuel_instrumented", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "lemma_Lib.Sequence.of_list_index", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_76ebfeadfe3c9c8f0c4cd972dcf30fb9", "refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_92ca0bc48157afddfbffad9d1595d489", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_bd2bfe2be0699d7dbe88f59eec7aa73c", "refinement_interpretation_Tm_refine_bf2fa1226f2c9a0f6671df3e80ddcb8e", "refinement_interpretation_Tm_refine_c046b844b424c31c6e5e249ececc788e", "refinement_interpretation_Tm_refine_c86aba5c6243e6b7f9a4b0ad41b4e9a0", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "typing_FStar.List.Tot.Base.index", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.maxint", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v", "typing_LowStar.ConstBuffer.as_mbuf", "typing_LowStar.ConstBuffer.q_preorder", "typing_Spec.ECDSAP256.Definition.p256_order_prime_list", "typing_Spec.ECDSAP256.Definition.prime_p256_order", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok", "typing_tok_LowStar.ConstBuffer.IMMUTABLE@tok" ], 0, "83f3f00ecd608062425daecd047748f9" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.order_inverse_buffer", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.CONST", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.CONST@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_heap_color", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.recallable", "equation_Lib.Buffer.witnessed", "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.ECDSA.prime_p256_order_inverse_seq", "function_token_typing_FStar.Monotonic.Heap.heap", "int_typing", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_225f262b1fc39e6f2640d04f361e62c3", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Lib.IntTypes.mk_int", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "960d83909e8d297f1bc07477d55daf28" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.order_buffer", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.CONST", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.Buffer.CONST@tok", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.HyperStack.ST.is_eternal_region", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_heap_color", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.recallable", "equation_Lib.Buffer.witnessed", "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.ECDSA.prime_p256_order_seq", "function_token_typing_FStar.Monotonic.Heap.heap", "int_typing", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_225f262b1fc39e6f2640d04f361e62c3", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.rid_freeable", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Lib.IntTypes.mk_int", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "19d65978c1062dd3272325d70556240d" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.add8_without_carry1", 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", "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.max_int", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "797a43fc4191ed89362f24c737d8298f" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.add8_without_carry1", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.P256.Felem.wide_as_nat", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Spec.P256.Definitions.wide_as_nat4", "int_inversion", "int_typing", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_c7df536c94c9b49c9149fb3f21ad016c", "refinement_interpretation_Tm_refine_f6e25f0e961ae531088e041fdcc67861", "typing_Hacl.Spec.P256.Felem.wide_as_nat", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "9c2c330e88f973963946efbfa5652732" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_montgomery_mult_1", 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, "557215284123fab6de54a1a3a0c1d439" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_montgomery_mult_1", 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, "49108d349f19204133e74b4a6f3f2ddb" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_montgomery_mult_1", 3, 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.Impl.ECDSA.MontgomeryMultiplication.prime", "equation_Hacl.Spec.ECDSAP256.Definition.prime_p256_order", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.nonzero", "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_571d9f74016be5357787170b42ecf913" ], 0, "8bb00a827cff138a8ea1a76941ac88de" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_montgomery_mult_result_less_than_prime_p256_order", 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, "c9c0e64855e1fc889a365a2a25dd4851" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_montgomery_mult_result_less_than_prime_p256_order", 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, "3c1457bac4158a1b2d450d1c85969ca7" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_montgomery_mult_result_less_than_prime_p256_order", 3, 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.nat", "equation_Prims.pos", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_d5ba4976e45f1806ec3b8267e5fb6f9d" ], 0, "b7dbb6be703f50699e3ef545ba57ebae" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_montgomery_mod_inverse_addition", 1, 2, 1, [ "@query", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "projection_inverse_BoxInt_proj_0" ], 0, "a14c3e73dd4a047ce58a380046f8cb5c" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_montgomery_mod_inverse_addition", 2, 2, 1, [ "@query", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "projection_inverse_BoxInt_proj_0", "true_interp" ], 0, "ddb91c342871c9895987e9cdf197ae74" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_montgomery_mod_inverse_addition2", 1, 2, 1, [ "@query", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "projection_inverse_BoxInt_proj_0" ], 0, "7acf108fd11121b9f6c860c5e219fe82" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_montgomery_mod_inverse_addition2", 2, 2, 1, [ "@query", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "projection_inverse_BoxInt_proj_0", "true_interp" ], 0, "6be03c82b2ceb6309c2169abee25894c" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.montgomery_multiplication_one_round_proof", 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_Spec.ECDSAP256.Definition.prime_p256_order", "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, "20c0d51c9f93d83971f745de02c15c33" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.montgomery_multiplication_one_round_proof", 2, 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.ECDSAP256.Definition.prime_p256_order", "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, "39ec07f232bc88a6d138996c99680a28" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.montgomery_multiplication_one_round_proof", 3, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.prime", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "refinement_interpretation_Tm_refine_0438740ce2081b11aff8bd34c3ab4147", "refinement_interpretation_Tm_refine_59f012ca5388d7bb5ddfd7d5db06b40a", "refinement_interpretation_Tm_refine_a84ad22af25f8c6b1555814df14c8d1e" ], 0, "7ff552a4b6f051786a4d9f2e5326bede" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.montgomery_multiplication_round", 1, 2, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_FStar.Monotonic.Heap.heap", "int_typing", "lemma_FStar.Map.lemma_ContainsDom", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Prims.pow2" ], 0, "8fa775d38e48f4b9d3057fdc0a553275" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.montgomery_multiplication_round", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.index.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.index.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.Buffer.MUT", "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", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Prims.Cons", "data_elim_Prims.Cons", "equality_tok_Lib.Buffer.MUT@tok", "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.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_stack_region", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.P256.Felem.as_nat_il", "equation_Hacl.Spec.P256.Felem.wide_as_nat", "equation_Hacl.Spec.P256.Felem.widefelem", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.eq_or_disjoint", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies0", "equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.stack_allocated", "equation_Lib.Buffer.union", "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.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.ECDSAP256.Definition.felem_seq_as_nat", "equation_Spec.ECDSAP256.Definition.p256_order_prime_list", "equation_Spec.P256.Definitions.as_nat4", "equation_Spec.P256.Definitions.wide_as_nat4", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_Lib.IntTypes.v_mk_int", "lemma_Lib.Sequence.of_list_index", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_regions", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "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", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_2c603a32dccef88313a514f059b6465a", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_70cd45088b125301ccac6ef654a56b45", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7a58fbf297e388448152b41221903b6a", "refinement_interpretation_Tm_refine_806119810bc08d323b64d62981ad893d", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_8cc8cfcb64d575010750a5c00af3e912", "refinement_interpretation_Tm_refine_92ca0bc48157afddfbffad9d1595d489", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a4cebef1b77740cb784abc3722606305", "refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e", "refinement_interpretation_Tm_refine_ba6eb85c87e18db53a236919f1fa7786", "refinement_interpretation_Tm_refine_bf2fa1226f2c9a0f6671df3e80ddcb8e", "refinement_interpretation_Tm_refine_c046b844b424c31c6e5e249ececc788e", "refinement_interpretation_Tm_refine_c86aba5c6243e6b7f9a4b0ad41b4e9a0", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "true_interp", "typing_FStar.List.Tot.Base.length", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Map.sel", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.unsigned", "typing_Lib.Sequence.create", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Prims.pow2", "typing_Spec.ECDSAP256.Definition.p256_order_prime_list", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "b71de2f69053c6d7a287148058c24423" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.montgomery_multiplication_round_twice", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "equation_Spec.ECDSAP256.Definition.widefelem", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Lib.IntTypes.uint64", "int_typing", "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_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "9de0bb44e1b284fda01496617aef50de" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.montgomery_multiplication_round_twice", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.Buffer.MUT", "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", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "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.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_Hacl.Spec.P256.Felem.wide_as_nat", "equation_Hacl.Spec.P256.Felem.widefelem", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.stack_allocated", "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.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "equation_Spec.P256.Lemmas.modp_inv2_prime", "equation_Spec.P256.Lemmas.modp_inv_prime", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_Lib.IntTypes.v_mk_int", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_70cd45088b125301ccac6ef654a56b45", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7e58423e952e9e2e163d684357f69578", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_Hacl.Spec.P256.Felem.wide_as_nat", "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Prims.pow2", "typing_tok_Lib.Buffer.MUT@tok", "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, "237324377d41add3eeb76995ac952f44" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.reduction_prime_2prime_with_carry", 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", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "9c8dd762bb5da3c08f7e6e5fae426275" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.reduction_prime_2prime_with_carry", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.Buffer.CONST", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.SEC", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Prims.Cons", "data_elim_Prims.Cons", "equality_tok_Lib.Buffer.CONST@tok", "equality_tok_Lib.Buffer.MUT@tok", "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.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.List.Tot.Base.tail", "equation_FStar.List.Tot.Base.tl", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_stack_region", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "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.Felem.as_nat", "equation_Hacl.Spec.P256.Felem.as_nat_il", "equation_Hacl.Spec.P256.Felem.felem", "equation_Hacl.Spec.P256.Felem.wide_as_nat", "equation_Hacl.Spec.P256.Felem.widefelem", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.eq_or_disjoint", "equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1", "equation_Lib.Buffer.stack_allocated", "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.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.ConstBuffer.live", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.ECDSAP256.Definition.felem_seq_as_nat", "equation_Spec.ECDSAP256.Definition.p256_order_prime_list", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "equation_Spec.P256.Definitions.as_nat4", "equation_Spec.P256.Definitions.wide_as_nat4", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd1", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Map.lemma_equal_elim", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_Lib.Buffer.mut_const_immut_disjoint", "lemma_Lib.IntTypes.v_mk_int", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.as_addr_gsub", "lemma_LowStar.Monotonic.Buffer.as_seq_gsub", "lemma_LowStar.Monotonic.Buffer.frameOf_gsub", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.live_gsub", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_buffer", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_regions", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "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", "projection_inverse_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_2c603a32dccef88313a514f059b6465a", "refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56c3919dda5153be7f87d90b0a6641c4", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_7074324d6f304dbb3152275fdefc45f5", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7a58fbf297e388448152b41221903b6a", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_92ca0bc48157afddfbffad9d1595d489", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a4cebef1b77740cb784abc3722606305", "refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e394e6ba5870f03674bfa9bf31f12fee", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "true_interp", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Map.sel", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Seq.Base.index", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Spec.P256.Felem.as_nat", "typing_Hacl.Spec.P256.Felem.wide_as_nat", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.index", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Prims.pow2", "typing_Spec.ECDSAP256.Definition.p256_order_prime_list", "typing_tok_Lib.Buffer.MUT@tok", "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, "f1f92a1ab707884ab3a1768e7d737dd4" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.reduction_prime_2prime_with_carry2", 1, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.ECDSAP256.Definition.felem", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat", "function_token_typing_Lib.IntTypes.uint64", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_tok_Lib.Buffer.MUT@tok" ], 0, "e888be2c1b945d9502646d79b576d1f4" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.reduction_prime_2prime_with_carry2", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.index.fuel_instrumented", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.index.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.Buffer.CONST", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.CONST@tok", "equality_tok_Lib.Buffer.MUT@tok", "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.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_stack_region", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Hacl.Spec.P256.Felem.as_nat", "equation_Hacl.Spec.P256.Felem.as_nat_il", "equation_Hacl.Spec.P256.Felem.felem", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1", "equation_Lib.Buffer.stack_allocated", "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.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.ConstBuffer.live", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.ECDSAP256.Definition.felem_seq_as_nat", "equation_Spec.ECDSAP256.Definition.p256_order_prime_list", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "equation_Spec.P256.Definitions.as_nat4", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Map.lemma_equal_elim", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_Lib.Buffer.mut_const_immut_disjoint", "lemma_Lib.IntTypes.v_mk_int", "lemma_Lib.Sequence.of_list_index", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_regions", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "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", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_2c603a32dccef88313a514f059b6465a", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56c3919dda5153be7f87d90b0a6641c4", "refinement_interpretation_Tm_refine_76ebfeadfe3c9c8f0c4cd972dcf30fb9", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_797d93795d485c2b0aa8ff1212f28f83", "refinement_interpretation_Tm_refine_7a58fbf297e388448152b41221903b6a", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_92ca0bc48157afddfbffad9d1595d489", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a4cebef1b77740cb784abc3722606305", "refinement_interpretation_Tm_refine_ab0deff5665fa4f9a3378f0a4ef6c9d5", "refinement_interpretation_Tm_refine_ae26262041daee30ae9f965181e5bf8c", "refinement_interpretation_Tm_refine_b47cabb890633249ae7f38d35cac724e", "refinement_interpretation_Tm_refine_bf2fa1226f2c9a0f6671df3e80ddcb8e", "refinement_interpretation_Tm_refine_c046b844b424c31c6e5e249ececc788e", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e394e6ba5870f03674bfa9bf31f12fee", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Seq.Base.index", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Spec.P256.Felem.as_nat", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.as_seq", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.ECDSAP256.Definition.p256_order_prime_list", "typing_tok_Lib.Buffer.MUT@tok", "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, "155e6ba5c6a82592383069a09f18696f" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_reduction1", 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, "a6e319ab0471c47ef57b9babd3b2460a" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_reduction1", 2, 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, "7c33108fd3f00401adad21b2683c9814" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_reduction1", 3, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "int_inversion", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_207bd418030414c32f7ebbc47cc48626", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_f87dcd46f42556e5a7ee78484f2b856d" ], 0, "43dd21e4504004239ae5afbb49e5da98" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.reduction_prime_2prime_order", 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", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "90f630561cf5017dcb8bb4f2923842f9" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.reduction_prime_2prime_order", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.Buffer.CONST", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.PUB", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Prims.Cons", "data_elim_Prims.Cons", "equality_tok_Lib.Buffer.CONST@tok", "equality_tok_Lib.Buffer.MUT@tok", "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.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.List.Tot.Base.tail", "equation_FStar.List.Tot.Base.tl", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_Hacl.Spec.P256.Felem.as_nat", "equation_Hacl.Spec.P256.Felem.as_nat_il", "equation_Hacl.Spec.P256.Felem.felem", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1", "equation_Lib.Buffer.stack_allocated", "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.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.ConstBuffer.live", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.ECDSAP256.Definition.felem_seq_as_nat", "equation_Spec.ECDSAP256.Definition.p256_order_prime_list", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "equation_Spec.P256.Definitions.as_nat4", "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_Lib.Buffer.mut_const_immut_disjoint", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_buffer", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_regions", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "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_Prims.Cons_a", "projection_inverse_Prims.Cons_hd", "projection_inverse_Prims.Cons_tl", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_2c603a32dccef88313a514f059b6465a", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56c3919dda5153be7f87d90b0a6641c4", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_7d84b8f3dff73d3cc195fbe597f5a194", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_92ca0bc48157afddfbffad9d1595d489", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_a4ca11e37f2e4f5b767a88d1f70ab6a7", "refinement_interpretation_Tm_refine_a4cebef1b77740cb784abc3722606305", "refinement_interpretation_Tm_refine_c86aba5c6243e6b7f9a4b0ad41b4e9a0", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "typing_FStar.List.Tot.Base.index", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length", "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.index", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.ECDSAP256.Definition.p256_order_prime_list", "typing_Spec.ECDSAP256.Definition.prime_p256_order", "typing_tok_Lib.Buffer.MUT@tok", "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, "e09f7ec39b90ae57ff83815feecebf6a" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.upload_k0", 1, 2, 1, [ "@MaxFuel_assumption", "@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", "equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing", "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", "token_correspondence_Prims.pow2.fuel_instrumented", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "5605e7fafd1163f1d150491157a62ee8" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.upload_k0", 2, 2, 1, [ "@MaxFuel_assumption", "@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.U32", "constructor_distinct_Lib.IntTypes.U64", "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", "equation_Spec.P256.Lemmas.elem", "equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing", "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_c1424615841f28cac7fc34e92b7ff33c", "token_correspondence_Prims.pow2.fuel_instrumented" ], 0, "646ba8bd666da6a115f4b69a50196203" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.fromDomain_", 1, 2, 1, [ "@query", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.prime", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0" ], 0, "54b3ab51d8962230a27c02ad4285d61e" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.toDomain_", 1, 2, 1, [ "@query", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0" ], 0, "44985f3de9001e65160fe5b747c84b67" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemmaFromDomain", 1, 2, 1, [ "@query", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "projection_inverse_BoxInt_proj_0" ], 0, "746d4f7c6ff805929634b0cb944ef76d" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemmaFromDomain", 2, 2, 1, [ "@query", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.fromDomain_" ], 0, "02eb7438cdea5b2bd03efbc5549268f3" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemmaToDomain", 1, 2, 1, [ "@query" ], 0, "79ccf7c32f6880a512f82f81c89719df" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemmaToDomain", 2, 2, 1, [ "@query", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.toDomain_" ], 0, "2de879e17a8c42ce067d2e8eb8bc011d" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemmaFromDomainToDomain", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.fromDomain_", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.prime", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.toDomain_", "equation_Prims.nat", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "int_inversion", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_90894f9bd6b7bb484068df7ac41cb0c5", "true_interp" ], 0, "55cf44939899bd5c779d477d228fdacc" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.multiplicationInDomain", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.prime", "equation_Prims.nat", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "int_inversion", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9b8144253a2faa447799216d63b2141e" ], 0, "6841bc3e6397c42ce2becd7d0ce75351" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.multiplicationInDomain", 2, 2, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.prime", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.toDomain_", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "int_inversion", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9b8144253a2faa447799216d63b2141e", "true_interp" ], 0, "77a3cc81692e1c0f4bbcf196786b4072" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.inDomain_mod_is_not_mod", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "int_inversion", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "63912e7d84c9032a1ba52c7f4364e8eb" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.inDomain_mod_is_not_mod", 2, 2, 1, [ "@query", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.toDomain_", "primitive_Prims.op_Modulus" ], 0, "1fce2af6451d089b27c214483d2bd7cf" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemmaToDomainFromDomain", 1, 2, 1, [ "@query" ], 0, "99fa0483db0e8f7909a0566871d2f4b4" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemmaToDomainFromDomain", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.fromDomain_", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.prime", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.toDomain_", "equation_Prims.nat", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "int_inversion", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_90894f9bd6b7bb484068df7ac41cb0c5", "true_interp" ], 0, "6ae3e6e27dfc412d1661bb0f857fac4a" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.montgomery_multiplication_ecdsa_module", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "d4d7549d29c54d1e1aacbe82da666baf" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.montgomery_multiplication_ecdsa_module", 2, 2, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query", "assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "bool_inversion", "bool_typing", "constructor_distinct_Lib.Buffer.MUT", "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", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "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.HyperStack.ST.equal_domains", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.Monotonic.Heap.equal_dom", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.is_stack_region", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_FStar.UInt.max_int", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.fromDomain_", "equation_Hacl.Impl.ECDSA.MontgomeryMultiplication.prime", "equation_Hacl.Spec.P256.Felem.as_nat", "equation_Hacl.Spec.P256.Felem.felem", "equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.eq_or_disjoint", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.Buffer.stack_allocated", "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.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro", "lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_InDomUpd2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain", "lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl", "lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset", "lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv", "lemma_Lib.IntTypes.v_mk_int", "lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer", "lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint", "lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_r", "lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2", "lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_none", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region", "lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_", "lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards", "lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_", "lemma_LowStar.Monotonic.Buffer.loc_union_comm", "lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim", "lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak", "lemma_LowStar.Monotonic.Buffer.modifies_loc_includes", "lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "lemma_LowStar.Monotonic.Buffer.popped_modifies", "lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in", "lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2", "refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_41f4533e602a16eddff1bda29b59239b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_56c3919dda5153be7f87d90b0a6641c4", "refinement_interpretation_Tm_refine_69a791d840c29995ad167402206cfbbf", "refinement_interpretation_Tm_refine_7074324d6f304dbb3152275fdefc45f5", "refinement_interpretation_Tm_refine_70cd45088b125301ccac6ef654a56b45", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_eed1d421faaa74a5f4114a511f0aa2eb", "refinement_interpretation_Tm_refine_f97c033d7b9efe762de97a7797c14ad6", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "token_correspondence_Prims.pow2.fuel_instrumented", "true_interp", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp", "typing_FStar.Monotonic.HyperHeap.mod_set", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperHeap.root", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_rid_ctr", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.Monotonic.HyperStack.is_stack_region", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Set.complement", "typing_FStar.Set.mem", "typing_FStar.Set.singleton", "typing_FStar.Set.union", "typing_Lib.Buffer.loc", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs", "typing_LowStar.Monotonic.Buffer.as_addr", "typing_LowStar.Monotonic.Buffer.frameOf", "typing_LowStar.Monotonic.Buffer.loc_addresses", "typing_LowStar.Monotonic.Buffer.loc_buffer", "typing_LowStar.Monotonic.Buffer.loc_none", "typing_LowStar.Monotonic.Buffer.loc_not_unused_in", "typing_LowStar.Monotonic.Buffer.loc_regions", "typing_LowStar.Monotonic.Buffer.loc_union", "typing_Prims.pow2", "typing_tok_Lib.Buffer.MUT@tok", "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, "073a03d6b959d7d4d880b86ff2f3438d" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.felem_add", 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", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "6b5df43df35730063e3359807ab3b3de" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.felem_add", 2, 2, 1, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Lib.Buffer.MUT", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.Buffer.MUT@tok", "equation_Hacl.Spec.P256.Felem.as_nat", "equation_Hacl.Spec.P256.Felem.felem", "equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.eq_or_disjoint", "equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.live", "equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies", "equation_Lib.IntTypes.uint64", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "function_token_typing_Lib.IntTypes.uint64", "int_inversion", "int_typing", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans", "lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains", "lemma_LowStar.Monotonic.Buffer.loc_includes_refl", "lemma_LowStar.Monotonic.Buffer.modifies_trans_linear", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_263d79e9f007855439e3ae995917b369", "refinement_interpretation_Tm_refine_573b33f33efdd29c4592319957948c79", "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b", "refinement_interpretation_Tm_refine_b7d182c5b613510e1104b690c3ea97a0", "typing_Lib.Buffer.loc", "typing_LowStar.Buffer.trivial_preorder", "typing_tok_Lib.Buffer.MUT@tok" ], 0, "a547eeffc14722efb240384c79f07b3e" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_felem_add", 1, 2, 1, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "int_inversion", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2" ], 0, "cc53d9c9260a2d7c1e95410fb0ebe30a" ], [ "Hacl.Impl.ECDSA.MontgomeryMultiplication.lemma_felem_add", 2, 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.Impl.ECDSA.MontgomeryMultiplication.prime", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.ECDSAP256.Definition.prime_p256_order", "equation_Spec.P256.Lemmas.modp_inv2_prime", "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", "token_correspondence_Prims.pow2.fuel_instrumented" ], 0, "2930d975cec5d5871d89686165bbaccd" ] ] ]