[ "Ø^¨\\º4Ò\nã\u0005ÄaZŒ7¯", [ [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_f", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.SEC@tok", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Lib.IntTypes.int_t", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "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_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e8ec9f27c00e08c9a32e383955df3d5c", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb" ], 0, "e6537d876a43f30b22db86c6b223b66f" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_f", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "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_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_e8ec9f27c00e08c9a32e383955df3d5c", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "27490b2b947576aad9e436921479652a" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_f", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e8ec9f27c00e08c9a32e383955df3d5c", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "2e2de04f6431927ff5e88476f19b25e2" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71" ], 0, "327735065826a9a99ca60af1fbfe79d4" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "0c8e79e7b9c1144c1b1fbe7c2b9f5256" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont", 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.U32", "constructor_distinct_Lib.IntTypes.U64", "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_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_a470234b9939a538397a3051f3b2cf4b", "refinement_interpretation_Tm_refine_a730e7ac31ab2703a9c74950a7c16d24", "refinement_interpretation_Tm_refine_bd34b6ee8923da3d95aece6692120777", "refinement_interpretation_Tm_refine_c057ac40f7bf966f2932d6b0a909151d", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_Lib.IntTypes.bits", "typing_Prims.pow2", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok" ], 0, "52dcef4e9bb9661731aea15413cd1218" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct_f", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71" ], 0, "b21061ee91b6835306994424e90a41d6" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct_f", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71" ], 0, "7e75f85bb092db73998f686c84472b72" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct_f", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.S128", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7fa293acee7f8425377292e7525d7fa3", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "c7a74d2a593632380544a1325768a292" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_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", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "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_965b2daf0a7dd1f908f4b5382342cc71", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "05fda003e2e9d54e1c626d703df88b42" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71" ], 0, "ea5d420f62837880a182a86c55fbae82" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition", "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_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb" ], 0, "1cffd41086af6dd74b375bf6042ae7d9" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_f_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_a927208ed63cb8d3ef190387bdd1e099", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e8ec9f27c00e08c9a32e383955df3d5c", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "2a6c198c58401742415ee577899085eb" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_f_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "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_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_e8ec9f27c00e08c9a32e383955df3d5c" ], 0, "4d89c8ec4bcae863986dd97a28d6ad4a" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_f_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_f", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0b72b617030921a422a8020811c2f320", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5ddafc4629d779ca5a742c96d316f7ad", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_8d2a2bad1c04567ef81429a7f36ab1cf", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_a927208ed63cb8d3ef190387bdd1e099", "refinement_interpretation_Tm_refine_b979979ca077136e99c9afcce0253c72", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_ccbef96ee6e044a9cf0b4353c2d1f06e", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e773a42934e56ab20618507a13aa2fbd", "refinement_interpretation_Tm_refine_e8ec9f27c00e08c9a32e383955df3d5c", "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.Sequence.sub", "typing_Lib.Sequence.update_sub", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "7634958a26020b2e7dc93e9940a87ea1" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_map", 1, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71" ], 0, "210808b7fbf5d9649244c6f7fc793dd9" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_map", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71" ], 0, "8bf3d0571670c0dd36bf8f8ed7c91baa" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_map", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb" ], 0, "8a68945fa735f6a1cf41b131036deff9" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_step_lemma", 1, 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.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "int_inversion", "l_and-interp", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_a927208ed63cb8d3ef190387bdd1e099", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_e8ec9f27c00e08c9a32e383955df3d5c", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok" ], 0, "ebf9d46c432b1c9bf3a96fe0feda720f" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_step_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "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_965b2daf0a7dd1f908f4b5382342cc71", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "6806a29061eea4b671617532edea12e7" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_step_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "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", "eq2-interp", "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.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.PrecompTable.bn_mod_precomp_table_mont_f", "equation_Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_map", "equation_Hacl.Spec.Exponentiation.Lemmas.mod_precomp_table_mont_f", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.Seq.Base.lemma_index_upd2", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThan", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_48890b928ce2d13056519fd2ac8d6dfa", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_a927208ed63cb8d3ef190387bdd1e099", "refinement_interpretation_Tm_refine_ccbef96ee6e044a9cf0b4353c2d1f06e", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d7ce5cfe8fd0dba8bf9d6500c54275d4", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292", "refinement_interpretation_Tm_refine_e8ec9f27c00e08c9a32e383955df3d5c", "refinement_interpretation_Tm_refine_ff3e40049a5afe27cc01ddfed980280d", "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.bn_v", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Hacl.Spec.Montgomery.Lemmas.mont_mul", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.index", "typing_Lib.Sequence.to_seq", "typing_Lib.Sequence.upd", "typing_Lib.Sequence.update_sub", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "eafba37f426135e7029066e5b4321d5c" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_loop_lemma", 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.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "int_inversion", "l_and-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6a3d9edb35cea3c3fa1f664ccbf59f39", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9012960530905b9fe2afee19e88cb546", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "73ace78d72f870fcf05522d1b191aa26" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_loop_lemma", 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.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Montgomery.bn_mont_pre", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "int_inversion", "l_and-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6a3d9edb35cea3c3fa1f664ccbf59f39", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9012960530905b9fe2afee19e88cb546", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f6619dea7abecd7a6957543e333c02e2", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "93f59cdc4904755379b257dfc7614fbe" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_loop_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "binder_x_13a49770a881677ceb1fe0f760f300ae_1", "binder_x_536d7216fb953a6c9e4a31bd8074650d_8", "binder_x_5bab3103cc045fd8cc8c0a7e94360049_4", "binder_x_69ada7bcf4dba8a70008ac2bf509ddb3_3", "binder_x_841b4d802a58cc8b28cf8b35864b4d5d_0", "binder_x_a743394fa4e4181e93be3c068d2aecf1_6", "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", "eq2-interp", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equality_tok_Prims.LexTop@tok", "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.PrecompTable.bn_mod_precomp_table_mont_map", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "l_and-interp", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThan", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2bfa8e0d39b8f491484e178c7c88c452", "refinement_interpretation_Tm_refine_32748f04bf9bf8de58da6a3993af7852", "refinement_interpretation_Tm_refine_3c217135469ccc7f2e4192e1eadb500e", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_939eed286319c2daa0c3b2eeab7dbed5", "refinement_interpretation_Tm_refine_c6608830fc23ad951ca334775a047625", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f2d9bb9ff72cb11d92585c6faaa31b37", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "well-founded-ordering-on-nat" ], 0, "27945ae66144f42bc94ee2d75f8c7014" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_lemma", 1, 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.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.Montgomery.bn_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", "equation_Prims.squash", "l_and-interp", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok" ], 0, "262f7a4ba42c84e9b74f764762a0f079" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5" ], 0, "ff4bd98eec043b446a6c1649751c4d79" ], [ "Hacl.Spec.Bignum.PrecompTable.bn_mod_precomp_table_mont_lemma", 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.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.PrecompTable.bn_mod_precomp_table_mont", "equation_Hacl.Spec.Exponentiation.Lemmas.mod_precomp_table_mont", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Lib.IntTypes.uint64", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0b72b617030921a422a8020811c2f320", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb", "refinement_interpretation_Tm_refine_1059f3601e6540d4a9b110371823333e", "refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106", "refinement_interpretation_Tm_refine_3731b8a78f0cea3bca96f9aeb24159ab", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_a0fa57358bb311df36ee743e70c2748d", "refinement_interpretation_Tm_refine_a28fb6569ac566f9141f5837f4f19069", "refinement_interpretation_Tm_refine_a470234b9939a538397a3051f3b2cf4b", "refinement_interpretation_Tm_refine_a730e7ac31ab2703a9c74950a7c16d24", "refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877", "refinement_interpretation_Tm_refine_a8dd452eb4cbfa4ea73050551c16fb42", "refinement_interpretation_Tm_refine_b2bf69252ac97b7d15e9de94ed509b9d", "refinement_interpretation_Tm_refine_bd34b6ee8923da3d95aece6692120777", "refinement_interpretation_Tm_refine_c057ac40f7bf966f2932d6b0a909151d", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_ca4489e15cf23a81ab8fc8bd779ec12d", "refinement_interpretation_Tm_refine_ccbef96ee6e044a9cf0b4353c2d1f06e", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v", "typing_Lib.Sequence.sub", "typing_Lib.Sequence.update_sub", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "b14cfd682dc18db6ebc8a735767598ac" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct_f_lemma", 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.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_FStar.UInt.min_int", "equation_Hacl.Spec.Bignum.Base.size_to_limb", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_24a7b28458ba679bb56000984769c285", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7fa293acee7f8425377292e7525d7fa3", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.size_to_uint64", "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, "4f6d161d879a26cef012d34f240a7af0" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct_f_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "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_965b2daf0a7dd1f908f4b5382342cc71", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "20627a105abd988c6242478c953a7354" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct_f_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "constructor_distinct_Lib.IntTypes.S128", "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", "disc_equation_Lib.IntTypes.S128", "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_Hacl.Spec.Bignum.Base.mask_values", "equation_Hacl.Spec.Bignum.Base.size_to_limb", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Hacl.Spec.Bignum.PrecompTable.table_select_ct_f", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.ones_v", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.eq_mask_lemma", "lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_032bf6a48f5060ca879f2d84d403b4fa", "refinement_interpretation_Tm_refine_0c6907d271a3f37ff8fbfce1f7abda4e", "refinement_interpretation_Tm_refine_1f338ca89b14fdf09b67051d08dca8db", "refinement_interpretation_Tm_refine_24a7b28458ba679bb56000984769c285", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_636b85ce1bb0908038f96551e60067dc", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_7fa293acee7f8425377292e7525d7fa3", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d13c5132af51f62dfb7018a438f66ab7", "refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.ones", "typing_Lib.IntTypes.size_to_uint32", "typing_Lib.IntTypes.size_to_uint64", "typing_Lib.IntTypes.v", "typing_Lib.IntTypes.zeros", "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, "a32a4f9b0b29b0a388bed55b15d81ceb" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct_loop_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_636b85ce1bb0908038f96551e60067dc", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "86fadc73cc2419bf44da852a7e4fb581" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct_loop_lemma", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.pos", "primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71" ], 0, "5ea0122fe1dffc9f6ccc315bbca583cd" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct_loop_lemma", 3, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S32", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.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.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq", "equation_Prims.nat", "equation_Prims.pos", "function_token_typing_Prims.__cache_version_number__", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_07b3bed5187f7ef145280643657b08b6", "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_636b85ce1bb0908038f96551e60067dc", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_adc6eab6a62a089a838b34b2e2ffa637", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_cf74cf5c1e7834b84db9cc7ebce886a3", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "refinement_interpretation_Tm_refine_ef1d13dedf1b6e95e0ada55dfa2b296f", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "55d18a3cddbba114ecf2ffb2b4fd4da8" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct_lemma", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U64", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U64@tok", "equation_Hacl.Spec.Bignum.Definitions.lbignum", "equation_Hacl.Spec.Bignum.Definitions.limb", "equation_Hacl.Spec.Bignum.Definitions.limb_t", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_636b85ce1bb0908038f96551e60067dc", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71", "refinement_interpretation_Tm_refine_cfc744b198940c21e3f980c86ac17a92", "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42", "typing_FStar.Seq.Base.length", "typing_Hacl.Spec.Bignum.Definitions.limb", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "9d954272e80e94c8619f26fcad1250de" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct_lemma", 2, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "equation_Prims.nat", "equation_Prims.pos", "lemma_FStar.UInt.pow2_values", "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_965b2daf0a7dd1f908f4b5382342cc71", "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok" ], 0, "fd72d55ff5821fce7d3d119a3104e12b" ], [ "Hacl.Spec.Bignum.PrecompTable.table_select_ct_lemma", 3, 0, 0, [ "@MaxIFuel_assumption", "@query", "equation_Hacl.Spec.Bignum.PrecompTable.table_select_ct", "equation_Prims.nat", "equation_Prims.pos", "int_inversion", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_965b2daf0a7dd1f908f4b5382342cc71" ], 0, "83f1a6a9b5a5e29bfee2b0e97689f675" ] ] ]