[ "\u0012rW\r.@sUŖ\u007f", [ [ "Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Bignum.bn_len", "equation_Prims.pos", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a" ], 0, "fcd863f0eaac2ccbff43a42f64a908aa" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.bn_len", "equation_Prims.pos", "primitive_Prims.op_Modulus", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8cbce6535fc28d41b6742c7f2b4ce0c4", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a" ], 0, "b75751db1b01d4886d861b3ca2ba09f3" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.mk_to_nat_mont_ll_comm_monoid", 1, 0, 0, [ "@query" ], 0, "9185d25e276603ec76c09077f9562fee" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.mk_to_nat_mont_ll_comm_monoid", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "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_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre", "equation_Hacl.Spec.Bignum.bn_len", "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.pos", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_6aa2b79520619ef0bdf5455f54002473", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok" ], 0, "d1f334d698725a7a78df550ba5152492" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_almost_mont_one", 1, 0, 0, [ "@query" ], 0, "d1f136dd26dbcbbdcf5329e483373228" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_almost_mont_one", 2, 0, 0, [ "@query" ], 0, "9341ef043aa30a135802d358ec67efd0" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_almost_mont_one", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "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.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.mk_to_nat_mont_ll_comm_monoid", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.MontExponentiation.mk_to_nat_mont_ll_comm_monoid", "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre", "equation_Hacl.Spec.Bignum.bn_len", "equation_Hacl.Spec.Exponentiation.Lemmas.mk_nat_mont_ll_comm_monoid", "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.pos", "function_token_typing_Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", "interpretation_Tm_abs_c33b6c12dcce6304188e526d2cdcaec2", "proj_equation_Lib.Exponentiation.Mkcomm_monoid_one", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_refl", "projection_inverse_BoxInt_proj_0", "projection_inverse_Lib.Exponentiation.Mkcomm_monoid_one", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_refl", "refinement_interpretation_Tm_refine_6aa2b79520619ef0bdf5455f54002473", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f9783c64b447f67f7fc4109eaca9c1a8", "token_correspondence_Spec.Exponentiation.__proj__Mkto_comm_monoid__item__refl", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok" ], 0, "95aa8454bcf18943e11f8f034b358f59" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_almost_mont_mul", 1, 0, 0, [ "@query" ], 0, "2cc79452aeff48f95b9beffc482c1972" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_almost_mont_mul", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Bignum.bn_len", "equation_Prims.pos", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a" ], 0, "00225448982bc4b64862f8c82cdf8138" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_almost_mont_mul", 3, 0, 0, [ "@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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.mk_to_nat_mont_ll_comm_monoid", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre", "equation_Hacl.Spec.Bignum.bn_len", "equation_Hacl.Spec.Exponentiation.Lemmas.mk_nat_mont_ll_comm_monoid", "equation_Hacl.Spec.Exponentiation.Lemmas.mont_mul_ll", "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Lib.Exponentiation.Mkcomm_monoid_mul", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_a_spec", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_refl", "projection_inverse_BoxInt_proj_0", "projection_inverse_Lib.Exponentiation.Mkcomm_monoid_mul", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_a_spec", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_refl", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6aa2b79520619ef0bdf5455f54002473", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "token_correspondence_Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", "token_correspondence_Hacl.Spec.Exponentiation.Lemmas.mont_mul_ll", "token_correspondence_Lib.Exponentiation.__proj__Mkcomm_monoid__item__mul", "token_correspondence_Spec.Exponentiation.__proj__Mkto_comm_monoid__item__refl", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "ca56ba926709aef363109070cbc5a2d2" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_almost_mont_sqr", 1, 0, 0, [ "@query" ], 0, "6c22ba8b3448e49519cc40c8dbbb5b3f" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_almost_mont_sqr", 2, 0, 0, [ "@query" ], 0, "1f2ec2a4a6a5a49d62e490fc064aba83" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_almost_mont_sqr", 3, 0, 0, [ "@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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.mk_to_nat_mont_ll_comm_monoid", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre", "equation_Hacl.Spec.Bignum.bn_len", "equation_Hacl.Spec.Exponentiation.Lemmas.mk_nat_mont_ll_comm_monoid", "equation_Hacl.Spec.Exponentiation.Lemmas.mont_mul_ll", "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Lib.Exponentiation.Mkcomm_monoid_mul", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_a_spec", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_refl", "projection_inverse_BoxInt_proj_0", "projection_inverse_Lib.Exponentiation.Mkcomm_monoid_mul", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_a_spec", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_refl", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6aa2b79520619ef0bdf5455f54002473", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "token_correspondence_Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", "token_correspondence_Hacl.Spec.Exponentiation.Lemmas.mont_mul_ll", "token_correspondence_Lib.Exponentiation.__proj__Mkcomm_monoid__item__mul", "token_correspondence_Spec.Exponentiation.__proj__Mkto_comm_monoid__item__refl", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "3ac8c934d720621adacdb6165331b79c" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.mk_bn_almost_mont_concrete_ops", 1, 0, 0, [ "@query" ], 0, "046e2fc9f787b27ba632dac823f93ef7" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.mk_bn_almost_mont_concrete_ops", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Bignum.bn_len", "equation_Prims.pos", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a" ], 0, "31cbbc36a69b4f8ec1b3df443d399758" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_exp_almost_mont_st", 1, 0, 0, [ "@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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre", "equation_Hacl.Spec.Bignum.bn_len", "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6aa2b79520619ef0bdf5455f54002473", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f9783c64b447f67f7fc4109eaca9c1a8", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "7e0dd8c3dc03672fc1e20abd24f32ef4" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_exp_almost_mont_bm_vartime", 1, 0, 0, [ "@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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "d1150b75b56dc46f38b8c715878ee4cc" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_exp_almost_mont_bm_vartime", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Spec.Exponentiation_interpretation_Tm_arrow_93c58cb2bd28a0e7c7f19c9616228a46", "Spec.Exponentiation_interpretation_Tm_arrow_d85a86789890122f5dab8a3a2829d356", "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_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.mk_bn_almost_mont_concrete_ops", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.mk_to_nat_mont_ll_comm_monoid", "equation_Hacl.Spec.Bignum.Definitions.blocks0", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre", "equation_Hacl.Spec.Bignum.bn_len", "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Spec.Exponentiation.__proj__Mkto_comm_monoid__item__refl", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "proj_equation_Spec.Exponentiation.Mkconcrete_ops_to", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_a_spec", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_refl", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.Exponentiation.Mkconcrete_ops_to", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_a_spec", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_refl", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_20212b4b7beadd1362c27540269e989b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6aa2b79520619ef0bdf5455f54002473", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f9783c64b447f67f7fc4109eaca9c1a8", "token_correspondence_Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", "token_correspondence_Spec.Exponentiation.__proj__Mkto_comm_monoid__item__refl", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "8ea8ba216fb419b518d25d709c800036" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_exp_almost_mont_bm_consttime", 1, 0, 0, [ "@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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "8f6cc9f015aa857d6ccacdda24272dcd" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_exp_almost_mont_bm_consttime", 2, 0, 0, [ "@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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.mk_bn_almost_mont_concrete_ops", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.mk_to_nat_mont_ll_comm_monoid", "equation_Hacl.Spec.Bignum.Definitions.blocks0", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre", "equation_Hacl.Spec.Bignum.bn_len", "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.NatMod.nat_mod", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "proj_equation_Spec.Exponentiation.Mkconcrete_ops_to", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_a_spec", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_refl", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.Exponentiation.Mkconcrete_ops_to", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_a_spec", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_refl", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_20212b4b7beadd1362c27540269e989b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6aa2b79520619ef0bdf5455f54002473", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f9783c64b447f67f7fc4109eaca9c1a8", "token_correspondence_Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", "token_correspondence_Spec.Exponentiation.__proj__Mkto_comm_monoid__item__refl", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "c35b18cdefebb7073b03b829981c9f63" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_exp_almost_mont_fw", 1, 0, 0, [ "@query" ], 0, "0f70b3963999cf441e32255b091af169" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_exp_almost_mont_fw", 2, 0, 0, [ "@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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_c158ef7e1b13334232cd46aacb616360", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "da01f09e17baf8c6285549c4b0686a03" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_exp_almost_mont_fw", 3, 0, 0, [ "@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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.mk_bn_almost_mont_concrete_ops", "equation_Hacl.Spec.Bignum.AlmostMontExponentiation.mk_to_nat_mont_ll_comm_monoid", "equation_Hacl.Spec.Bignum.Definitions.blocks0", "equation_Hacl.Spec.Bignum.Definitions.bn_v", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre", "equation_Hacl.Spec.Bignum.bn_len", "equation_Hacl.Spec.Montgomery.Lemmas.mont_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.NatMod.nat_mod", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction", "proj_equation_Spec.Exponentiation.Mkconcrete_ops_to", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_a_spec", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid", "proj_equation_Spec.Exponentiation.Mkto_comm_monoid_refl", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.Exponentiation.Mkconcrete_ops_to", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_a_spec", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_comm_monoid", "projection_inverse_Spec.Exponentiation.Mkto_comm_monoid_refl", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_20212b4b7beadd1362c27540269e989b", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6aa2b79520619ef0bdf5455f54002473", "refinement_interpretation_Tm_refine_6d8406354946ff8e435b91c081840632", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_c158ef7e1b13334232cd46aacb616360", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_f9783c64b447f67f7fc4109eaca9c1a8", "token_correspondence_Hacl.Spec.Bignum.AlmostMontExponentiation.amm_refl", "token_correspondence_Spec.Exponentiation.__proj__Mkto_comm_monoid__item__refl", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "772965e3548edeb6ac716f161c56dcf8" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_exp_almost_mont_vartime", 1, 0, 0, [ "@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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "7098f5a5fd4eebe8a7deaf6f0528247c" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_exp_almost_mont_vartime", 2, 0, 0, [ "@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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.MontExponentiation.bn_exp_mont_vartime_threshold", "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_4", "primitive_Prims.op_LessThan", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "20092dc6c37e336a5b3d374f472646b7" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_exp_almost_mont_consttime", 1, 0, 0, [ "@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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "ecc42a70aa2a0d2f3f79607f0916c1a6" ], [ "Hacl.Spec.Bignum.AlmostMontExponentiation.bn_exp_almost_mont_consttime", 2, 0, 0, [ "@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.U1", "constructor_distinct_Lib.IntTypes.U16", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "constructor_distinct_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.MontExponentiation.bn_exp_mont_consttime_threshold", "equation_Hacl.Spec.Bignum.bn_len", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_4", "primitive_Prims.op_LessThan", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_9a3e47960c8f13c0402e1a809c52535a", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "d94dd22b16b91e3b7948accfba1288d0" ] ] ]